.. highlight:: python :linenothreshold: 50 .. _read-write-lock-label: ################################### Read-write lock ################################### .. image:: rwlock-config.svg :width: 450 px :align: center This section shows an application of Sesf for a single-process program. We start by informally describing a read-write-lock service. We give a candidate implementation (imp_0) and a simple user program to exercise any implementation. We formally define the service by a service program, first the abstract version and then a concrete version. The (concrete) service program can be driven by the user program. We define the corresponding servicetester program, first the abstract version and then a concrete version. The (concrete) servicetester can test any implementation. We end with two more candidate implementations, imp_1 and imp_2. A proof of correctness for each implementation is in a separate document, `rwlock.pdf <../../analysis/rwlock.pdf>`_ (in the correctness branch). .. We then give two more candidate implementations, imp_1 and imp_2. .. imp_0 and imp_2 implement the service except for one progress requirement (writers can starve). imp_1 implements the service fully. ----------------------------------- Intended service informally stated ----------------------------------- The read-write-lock service has four functions that can be called by local users in the environment (in the same address-space for now). - ``acqr()``: acquire a read lock. - Return only when no thread holds a write lock, else block. - Call only if the caller does not already hold a read or write lock. - ``relr()``: release a read lock. - Return indicates that the caller thread no longer holds a read lock. - Call only if the caller holds a read lock. - ``acqw()``: acquire a write lock. - Return only when no thread holds a read or write lock, else block. - Call only if the caller does not already hold a read or write lock. - ``relw()``: release a write lock. - Return indicates that the caller thread no longer holds a write lock. - Call only if the caller holds a write lock. - **Progress requirements:** - every ``acqr()`` call eventually returns if no user holds a read or write lock indefinitely. - every ``acqw()`` call eventually returns if no user holds a read or write lock indefinitely. Although the above is informal, it unambiguously describes the intended service of the distributed program. The function calls define the inputs. The function returns define the outputs. The constraints on function calls and return values define the set of acceptable inputs and outputs. Later we define it formally by a service program. ----------------------------------------- Candidate implementation ``Imp_0`` ----------------------------------------- .. automodule:: rwlock.imp_0.imp .. autoclass:: rwlock.imp_0.imp.Imp ---------------------- User program ---------------------- .. automodule:: rwlock.user .. autoclass:: rwlock.user.User ----------------------------------------- Service program (abstract version) ----------------------------------------- The intended service is formally defined by a service program (abstract version), specifically, a "pseudo-Python" class ``Service``. We say "pseudo-Python" because it has non-Python constructs (namely, ``CIC``, ``CU``, ``ROC``, ``RU``), which are explained below. Conceptually, the class is a program that can, at any point in its execution, receive any (and only an) acceptable input and can return any acceptable output. .. literalinclude:: ../../sesf/rwlock/service.ppy The class has four non-init functions: ``acqr()``, ``relr()``, ``acqw()`` and ``relw()``, corresponding to the four functions called by users of the service. The ``__init__`` function defines variables adequate to express when a non-init function can be called and when it can return. Every non-init function has four components: ``CIC``, short for **call input condition**; ``CU``, short for **call update**; ``ROC``, short for **return output condition**; and ``RU``, short for **return update**. The call input condition and call update make up the **input part**. It checks whether the function call is valid, and if so updates the instance variables. Specifically, when a thread comes to the call input condition, it does the following in one atomic step: evaluate the call condition; if true (which means the call is valid) execute the call update, else *abort*. The return output condition and return update make up the **output part**. It checks whether the function can return, and if so updates the instance variables and returns. Specifically, a thread atomically executes the return update only if the return condition holds, else it *blocks*. ----------------------------------------- Service program (concrete version) ----------------------------------------- The concrete version of the abstract service program is obtained by implementing the latter's non-Python constructs in Python. This can be easily done using locks and condition variables. Consider a function ``f`` in the pseudo-Python class: .. code-block:: python # pseudo-Python def f(self): CIC: ... CU: ... ROC: ... RU: ... Introduce a lock, say ``lck``, and an associated condition variable, say ``cond``. Then the psuedo-Python function ``f`` can be implemented by the following regular Python function ``f``. (``f.CIC`` refers to the body of ``CIC`` in pseudo-Python function ``f``; ditto for ``f.CU``, ``f.ROC``, ``f.RU``). .. code-block:: python # regular Python def f(self): # do_service_input with self.cond: if not f.CC(): raise Exception("call input condition violated") f.CU() self.cond.notify_all() # do_service_output with self.cond: while not f.RC(): self.cond.wait() f.RU() self.cond.notify_all() | For convenience, we go through an intermediate class before defining the concrete service program. .. automodule:: rwlock.serviceparts .. autoclass:: ServiceParts .. automodule:: rwlock.service .. autoclass:: Service --------------------------------------------------------- Running a user program on the service program --------------------------------------------------------- .. image:: rwlock-user+service-config.svg :width: 330 px :align: center .. automodule:: rwlock.service_imp .. autoclass:: Imp Here are the steps for running a user program, say ``user.py``, over the service program (instead of over an implementation), along with some details about what happens internally. The following commands are for working directory ``sesf/rwlock``. #. Start a Pyro4 **nameserver** if one is not already running: run ``python -m Pyro4.naming`` (or ``python -m Pyro4.naming &``). #. Start the rwlock service: run ``python service.py``. The service registers itself with the nameserver using the name `sesf.rwlock.service`, starts a Pyro4 **daemon** (to receive RPCs) in a separate thread, and waits to be contacted (by `service_imp`). #. Start the user program: run ``python user.py service_imp`` Instance `user.User` starts an instance `service_imp.Imp` as the rwlock implementation to drive. Any call made by `user.User` is redirected by `service_imp.Imp` to the running service program. After all the user threads have exited, `user.User` calls `service_imp.Imp.__end__` to terminate the running service process. -------------------------------------------- Servicetester program (abstract version) -------------------------------------------- The abstract servicetester program is obtained by "inverting" the abstract service program into a program that behaves as the most arbitrary (but valid) user of the service, one that any correct implementation should be able to handle. Essentially, we add a new parameter, say `imp`, pointing to the candidate implementation, and change each input function into an "output" function that calls the implementation's input function and checks whether the return value is one that the service could generate. .. |ss| raw:: html .. |se| raw:: html Function ``__init__`` is changed as follows: add parameter ``imp`` and store it in a new attribute ``self.imp``. Each function ``f`` in the abstract service class is changed as follows: .. raw:: html 
# pseudo-Python
   def f(self):
   def do_f(self, imp):
     CIC COC: ...           # output part
     CU: ...                #   "  "  "
     rval = imp.f(x)        # call to implementation
     ROC RIC: ...           # input part
     RU: ...                #   "  "  "
``COC`` is short for **call output condition**. The COC and CU make up the **output part**. It checks whether the function can be called, and if so updates the instance variables and makes the call. Specifically, a thread atomically executes the call update only if the call condition holds, else it *blocks*. ``RIC`` is short for **return output condition**. The RIC and RU make up the **input part**. It checks whether the function return is valid, and if so updates the instance variables. Specifically, when a thread comes to RIC, it does the following in one atomic step: evaluate RIC; if true (which means the return is valid) execute the return update, else *abort*. Assume there is an *unlimited supply of threads* to execute ``do_f``. .. literalinclude:: ../../sesf/rwlock/servicetester.ppy -------------------------------------------- Servicetester program (concrete version) -------------------------------------------- The concrete version of the abstract servicetester program is obtained by implementing the latter's non-Python constructs in Python, just as with the service program. Consider a function ``do_f`` in the pseudo-Python class: .. code-block:: python # pseudo-Python def do_f(self): COC: ... CU: ... self.imp.f() RIC: ... RU: ... The concrete version would be as follows, where ``lck`` is a lock, ``cond`` is an associated condition variable. .. code-block:: python # regular Python def do_f(self): # do_service_output with self.cond: while not f.COC(): self.cond.wait() f.CU() self.cond.notify_all() # call the matching implemenation function self.imp.f() # validate_service_input with self.cond: if not f.RIC(): raise Exception("return output condition violated") f_RU() self.cond.notify_all() | .. automodule:: rwlock.servicetester .. autoclass:: ServiceTester ------------------------------------------------------------------- Running the servicetester program on an implementation program ------------------------------------------------------------------- .. image:: rwlock-servicetester+imp-config.svg :width: 410 px :align: center .. automodule:: rwlock.test_imp .. autoclass:: TestImp Here are the steps for running the servicetester program over an implementation program, say ``imp_0.imp``, along with some details about what happens internally. The following commands are for working directory ``sesf/rwlock``. #. Start a Pyro4 **nameserver** if one is not already running: run ``python -m Pyro4.naming`` (or ``python -m Pyro4.naming &``). #. Start the rwlock test_imp wrapping implementation imp_0: run ``python test_imp.py --use imp_0.imp``. The test_imp registers itself with the nameserver using the name `sesf.rwlock.test_imp`, starts a Pyro4 **daemon** (to receive RPCs) in a separate thread, and waits to be contacted (by the servicetester). #. Start the servicetester program: run ``python servicetester.py `` The servicetester registers itself with the nameserver using the name `sesf.rwlock.servicetester`, starts a Pyro4 daemon (to receive any events that may be conveyed by the implementation being tested), and informs test_imp (via RPC) to activate implementation imp_0. After all the servicetester user threads have exited, the servicetester calls the test_imp's end_pyrodaemon to terminate test_imp. If imp_0 has a checker, the servicetester can load the checker and test its assertions when it receives events from the implementation. Run ``python servicetester.py --checker imp_0.checker`` ----------------------------------------- Candidate implementation ``Imp_1`` ----------------------------------------- .. automodule:: rwlock.imp_1.imp .. autoclass:: rwlock.imp_1.imp.Imp ----------------------------------------- Candidate implementation ``Imp_2`` ----------------------------------------- .. automodule:: rwlock.imp_2.imp .. autoclass:: rwlock.imp_2.imp.Imp .. .. note:: A **semaphore** has an internal "count" initialized to a non-negative integer. ``acquire()`` atomically decrements count, blocking if count is 0. ``release()`` atomically increments count.