.. highlight:: python
   :linenothreshold: 50

A distributed lock service spanning two locations
====================================================

This section defines a lock service spanning two locations,
identified by addresses 0 and 1.
At each address,
three functions can be called by a local user:

- ``acq()``: acquire the lock.

  - Return only if the remote user does not hold the lock,
    else block.
  - Call only if the local user does not hold the lock 
    and ``end()`` has not been called at any location.

- ``rel()``: release the lock.

  - Return ``None``.
  - Call only if the local user holds the lock

- ``end()``: end the lock.

  - Return ``None``.
  - Call only if the following holds at both locations:
    ``end()`` has not been called; there is no ongoing call;
    and the local user does not hold the lock.


Service program (abstract version)
------------------------------------------

The intended lock service is formally defined by
the pseudo-Python class ``Service`` in 
:doc:`distlock2.service.ppy </distlock2/distlock2_service>`.
As usual, parameter ``j`` in a function indicates the address of 
the corresponding function
(e.g., ``acq(j)`` corresponds to function ``acq()`` at address ``j``).

.. literalinclude:: ../../sesf/distlock2/service.ppy

Note that ``rel(j)`` gives up the lock in the call step.
So if ``rel(j)`` and ``acq(1-j)`` are both ongoing, 
``acq(1-j)`` can return before ``rel(j)`` returns.


Service program (concrete version)
------------------------------------------

The Python version of the service is in class 
``Service`` (same name in the pseudo-Python version):

.. automodule:: distlock2.service
.. autoclass:: Service



Service tester (abstract version)
--------------------------------------------

TODO


Service tester (concrete version)
--------------------------------------------

The servicetester is a program that can be used 
in place of the users of the service,
for testing an 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.


test_node
^^^^^^^^^^^^^^^^^^^^^

.. automodule:: distlock2.test_node
.. autoclass:: TestNode


servicetester
^^^^^^^^^^^^^^^^^^^^^

.. automodule:: distlock2.servicetester
.. autoclass:: ServiceTester


Implementation ``Imp_0`` (uses msgtransfer2 service)
----------------------------------------------------------------

.. image:: distlock2-config.svg
   :width: 650 px
   :align: center

.. automodule:: distlock2.imp_0.node

.. autoclass:: distlock2.imp_0.node.Node


.. automodule:: distlock2.imp_0.checker
.. autoclass:: Checker

|

**Running servicetester on an implementation using msgtransfer service**

Start a Pyro4 nameserver if one is not already running
(``python -m Pyro4.naming &``).

Start the msgtransfer2 service:

- ``python msgtransfer2/service.py``


Run the following two commands:

- ``python distlock2/test_node 2 0 --use imp_0.node 2 0``
- ``python distlock2/test_node 2 1 --use imp_0.node 2 1``
- Or instead of above, run
  ``python start_nodes.py 2 distlock/test_node.py --use imp_0.py``

Run the service tester with your checker:

- ``python distlock2/servicetester --checker imp_0.checker``