.. highlight:: python :linenothreshold: 50 A message-transfer service spanning N locations ================================================ .. image:: msgtransfer-config.svg :height: 230 px :align: center .. |gE| unicode:: U+02267 .. GREATER-THAN OVER EQUAL TO .. |geq| unicode:: U+2265 .. GREATER-THAN-OR-EQUAL-TO .. |gsim| unicode:: U+02273 .. GREATER-THAN OR EQUIVALENT TO This section extends the treatment in the :doc:`previous section ` to N locations, where N |geq| 2. We obtain service model and tester programs, and a distributed program that implements the service using TCP. For no good reason, there is also a program that plays the log of a test (:doc:`example video `). | Intended service informally stated ----------------------------------- The service spans N locations, identified by addresses 0, 1, ..., N-1, for any N |geq| 2. At each address ``j``, three functions are provided to the user: - ``send(k, msg)``: send message ``msg`` to address ``k``. - Return ``False`` only if the service is closed, else return ``True``. - Call only if no ``send()`` call is ongoing at address ``j`` and no previous ``send()`` call at address ``j`` has returned ``False``. - ``recv()``: receive a message sent at some other address. - Return ``(False,)`` only if the service is closed, return ``(True, msg)`` only if incoming message ``msg`` is available, else block. - Call only if no ``recv()`` call is ongoing at this address and no previous ``recv()`` call at this address has returned ``(False,)``. - For every address ``k``, messages received from ``k`` are in the order in which they were sent at address ``k``. But messages sent to ``j`` from different addresses can be received *interleaved in any order*. - ``end()``: Close the service. - Return ``None``. - Call only if ``end()`` has not been called at any address. | An implementation using TCP --------------------------------- .. automodule:: msgtransfer.imp_0.node .. autoclass:: Node | Starting the msgtransfer nodes from user nodes --------------------------------------------------- .. automodule:: sesf.msgtransfer.user_node .. autoclass:: UserNode | Service program (abstract version) ------------------------------------------------------------------ .. |sent_j,k| replace:: *sent*\ :sub:`j,k` .. |sent_N-1,0| replace:: *sent*\ :sub:`N-1,0` .. |sent_j,0| replace:: *sent*\ :sub:`j,0` .. |sent_1,0| replace:: *sent*\ :sub:`1,0` .. |sent_2,0| replace:: *sent*\ :sub:`2,0` .. |rcvd_k| replace:: *rcvd*\ :sub:`k` .. |rcvd_j,k| replace:: *rcvd*\ :sub:`j,k` .. |rcvd_j,0| replace:: *rcvd*\ :sub:`j,0` .. |rcvd_0| replace:: *rcvd*\ :sub:`0` .. |rcvd_1,0| replace:: *rcvd*\ :sub:`1,0` .. |rcvd_2,0| replace:: *rcvd*\ :sub:`2,0` .. |nrcvd_j,k| replace:: *nrcvd*\ :sub:`j,k` .. |nrcvd_j,0| replace:: *nrcvd*\ :sub:`j,0` Extending the (pseudo-Python) service program for :doc:`two addresses ` to more than 2 addresses has interesting consequences. Suppose the program maintains the following variables for every address j and k: |sent_j,k|, the sequence of messages sent at j to k; and |rcvd_k|, the sequence of messages received at k (from all addresses). Consider the receive function at say address 0. Its return condition would say that message *m* can be returned iff there is a merge *s* of |sent_1,0|, ..., |sent_N-1,0| such that |rcvd_0| concatentated with *m* is a prefix of *s*. This works but it's not convenient. The concrete service and servicetester programs would be computationally expensive. Using the abstract service and servicetester program in proofs would be messy. A better approach is to allow **internal non-determinism** in the service program. Instead of |rcvd_k|, suppose the program maintains |nrcvd_j,k|, the number of messages received at k from j. Also have an additional parameter j in the return part of ``recv(0)``. Then the return condition can say that message *m* can be returned iff there is a j such that *m* equals |sent_j,0|\ [|nrcvd_j,k|]. If more than one j satisfies this condition, a particular j is chosen **non-deterministically**. Furthermore, the non-determinism is **internal** because the environment does not see the chosen value of j (although it may able to infer it at some later point after receiving more messages). Using this approach, the service is formally defined by the pseudo-Python class ``Service`` in :doc:`msgtransfer.service.ppy `. As usual, each function has a parameter ``j`` identifying the address at which the function is located. .. .. literalinclude:: ../../sesf/msgtransfer/service.ppy | Service program (concrete version) ------------------------------------------------------ .. automodule:: msgtransfer.serviceparts .. autoclass:: ServiceParts Recall the internal parameter ``k`` in the return part of the pseudo-Python service function ``recv(j)``. Note what happens to it in the Python version of the service. In function ``recv_RCI(j,rval)``, the *input* version of ``recv(j).RC``, a value for ``k`` is provided by the implementation's ``rval``. In function ``recv_RCO(j)``, the *output* version of ``recv(j).RC``, the function generates a value for ``k``. | .. automodule:: sesf.msgtransfer.service_node .. autoclass:: Node .. automodule:: sesf.msgtransfer.service .. autoclass:: Service Note that function ``recv(j)`` does not return the value of the internal parameter ``k`` generated by ``recv_RCO(j)``. Running user nodes over the service ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The msgtransfer user node class can make use of the service model (instead of an implementation). - Start a Pyro4 nameserver if one is not already running: enter ``python -m Pyro4.naming &`` in a shell. - Run ``python service.py N``, to start the service program for ``N`` addresses. - Run ``python user_node.py N j --use service_node N j`` for ``j`` ranging over 0, 1, ..., N-1. (Or run ``python ../start_nodes.py N user_node.py --use service_node``.) | Servicetester (abstract version) -------------------------------------------- TODO Servicetester (concrete version) -------------------------------------------- Recall that the service tester is a program that can be used in place of the users of the service, typically for testing a (distributed) implementation of the service. For testing, each node of the implementation is wrapped in a "test node". The service tester makes RPC calls to the test nodes. A test node redirects incoming RPC calls to its implementation node. The service tester can also use a checker, if one is provided with the implementation, to check implementation-specific assertions. In this case, each implementation node can inform the servicetester of local events by calling the node's ``inform_tester()`` function. This function has no effect if the implementation node has not been started by a test node. | class TestNode ^^^^^^^^^^^^^^^^^^^^^ .. automodule:: msgtransfer.test_node .. autoclass:: TestNode | class ServiceTester ^^^^^^^^^^^^^^^^^^^^^ .. automodule:: msgtransfer.servicetester .. autoclass:: ServiceTester Note that the return part of function ``do_recv(j)`` expects the implementation-supplied ``rval`` to have a value for the internal parameter ``k`` of ``recv_RCI(j)``. This is easily achieved by having the servicetester include the value in the message it sends (in the call part of ``send(j)``); no modification to the implementation node's code is needed. | Checker for implementation imp_0 --------------------------------------------------------------- .. automodule:: msgtransfer.imp_0.checker .. autoclass:: Checker | Log player ------------ .. automodule:: msgtransfer.logplayer .. autoclass:: Artbase