1. Read-write lock

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 (in the correctness branch).

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

Module rwlock.imp_0.imp has class Imp that implements the read-write-lock service except that it allows writes to starve. To instantiate and drive Imp from rwlock/user.py, in the parent directory run “python user.py <num_threads> <num_ops> imp_0.imp”. Or instantiate Imp in your own program and drive it from there.

class rwlock.imp_0.imp.Imp

An implementation of the read-write-lock service except that acqw() can starve if there is a continuous stream of acqr(); relr()``s. It has four functions: ``acqr(), relr(), acqw() and relw(). It maintains the following variables:

• nr (int): number of threads holding a read lock; initially 0.
• nw (int): number of threads holding a write lock; initially 0.
• lck (lock): protects nr and nw.
• cvr (condition): to wait for nw equal to 0.
• cvw (condition): to wait for nr and nw equal to 0.

When a thread executes acqw(), it waits on cvw until nr and nw are 0, then increments nw and returns. At this point, no thread can acquire a write lock or a read lock. When a thread executes relw(), it decrements nw and returns.

When a thread executes acqr(), it waits on cvr until nw is 0, then increments nr and returns. At this point a thread can get a read lock but not a write lock. When a thread executes relr(), it decrements nr and returns.

User program

Module sesf.rwlock.user has class User that implements a user of the read-write-lock service. To drive a rwlock implementation, run

“python user.py <num_threads> <num_ops> <rwl_imp>”

where <rwl_imp> is the implementation module and any command line arguments (eg, imp_0.imp), to drive the implementation with num_threads user threads, each issuing num_ops read or write (randomly chosen) operations.

class rwlock.user.User(argv)

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.

# pseudo-Python module sesf.rwlock.service.ppy
# class Service is rwlock service (abstract version)

# threading.get_ident() returns the id of the calling thread
from threading import get_ident

class Service():
  def __init__(self):
    self.rset = set()  # ids of threads currently reading
    self.wset = set()  # ids of threads currently writing

  def acqr(self):
    CIC: get_ident() not in self.rset.union(self.wset)    # input part
    CU:  pass                                             #  "  "  "
    ROC: self.wset == set()                               # output part
    RU:  self.rset.add(get_ident())                       #  "  "  "

  def relr(self):
    CIC: get_ident() in self.rset                         # input part
    CU:  self.rset.remove(get_ident())                    #  "  "  "
    ROC: True                                             # output part
    RU:  pass                                             #  "  "  "

  def acqw(self):
    CIC: get_ident() not in self.rset.union(self.wset)    # input part
    CU:  pass                                             #  "  "  "
    ROC: self.wset == self.rset == set()                  # output part
    RU:  self.wset.add(get_ident())                       #  "  "  "

  def relw(self):
    CIC: get_ident() in self.wset                         # input part
    CU:  self.wset.remove(get_ident())                    #  "  "  "
    ROC: True                                             # output part
    RU:  pass                                             #  "  "  "


  progress assumption:
    # u, v range over thread ids
    L_1:  P_1  =>  ((v at acqr.ROC) leads-to (not v at acqr.ROC))  # acqr
    L_2:  ((v at relr.ROC) leads-to (not v at relr.ROC))           # relr
    L_3:  P_1  =>  ((v at acqw.ROC) leads-to (not v at acqw.ROC))  # acqw
    L_4:  ((v at relw.ROC) leads-to (not v at acqr.ROC))           # relw
    where
    P_1:  (u in union(rset, wset))  leads-to  (u not in union(rset, wset))

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:

# 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).

# 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.

Module rwlock.serviceparts has a class ServiceParts, which has a separate function for each component of each pseudo-Python function in the abstract service program.

class rwlock.serviceparts.ServiceParts

Anatomy of pseudo-Python class rwlock.service.Service. Has the same variables: rset and wset. For each non-init function f in the pseudo-Python class, has four functions: f_CIC, f_CU, f_ROC and f_RU.

Module rwlock.service has class Service, which is the concrete version of the read-write-lock service program.

class rwlock.service.Service

Read-write lock service (concrete version). Should be accessed via RPC (Pyro4) for testing a rwlock user program.

Maintains the following variables:

• serviceparts (obj): read-write-lock serviceparts
• lck, cond: lock and condition variable for atomicity of call and return parts.
• pyrodaemon: Pyro4 daemon object for handling RPC calls

Functions (all have random delays):

• acqr(): acquire a read lock; blocking.
• relr(): release a read lock; nonblocking.
• acqw(): acquire a write lock; blocking.
• relw(): release a write lock; nonblocking.

Running a user program on the service program

Module sesf.rwlock.service_imp has class Imp that has the signature of rwlock service and redirects incoming calls (from a rwlock user) to RPC calls to a running rwlock.service program. Class Imp also has a __end__ function (to be called by the rwlock user) that ends the running rwlock.service program.

class rwlock.service_imp.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.

1. Start a Pyro4 nameserver if one is not already running: run python -m Pyro4.naming (or python -m Pyro4.naming &).

2. 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).

3. Start the user program: run python user.py <num_threads> <num_ops> 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.

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:

# 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.

# pseudo-Python module sesf.rwlock.servicetester.ppy
# class ServiceTester is rwlock servicestester (abstract version)

# threading.get_ident() returns the id of the calling thread
from threading import get_ident

class ServiceTester:
  def __init__(self, imp):
    self.rset = set()
    self.wset = set()
    self.imp = imp

  def do_acqr(self):
    COC: get_ident() not in self.rset.union(self.wset)
    CU:  pass
    self.imp.acqr()
    RIC: self.wset == set()
    RU:  self.rset.add(get_ident())

  def do_relr(self):
    COC: get_ident() in self.rset
    CU:  self.rset.remove(get_ident())
    self.imp.relr()
    RIC: True
    RU:  pass
   
  def do_acqw(self):
    COC: get_ident() not in self.rset.union(self.wset)
    CU:  pass
    self.imp.acqw()
    RIC: self.wset == self.rset == set()
    RU:  self.wset.add(get_ident())
   
  def do_relw(self):
    COC: get_ident() in self.wset
    CU:  self.rset.remove(get_ident())
    self.imp.relw()
    RIC: True
    RU:  pass

  progress condition:
    <service.py progress assumption, but now it's a condition to be proved>

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:

# 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.

# 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()

Module sesf.rwlock.servicetester has class ServiceTester that implements the read-write-lock servicetester. This can test an implementation against the rwlock service and, optionally, against a checker with implementation-specific assertions.

For example, assuming a running Pyro4 nameserver and a running test_imp using rwlock.imp_0.imp,

python servicetester.py <num_threads> <num_ops> --checker imp_0.checker

tests the rwlock imp_0 implementation with num_threads threads each doing num_ops read or write operations, and imp_0.checker to evaluate implementation-specific assertions.

class rwlock.servicetester.ServiceTester(num_users, num_ops, checkermodule=None)

Read-write-lock servicetester to test an implementation, driving it with num_users user threads each doing num_ops (randomly chosen) read or write operations, and optionally using checkermodule.Checker. It maintains the following variables:

• num_users (int): number of user threads in testing
• num_ops (int): number of read or write operations per user thread.
• checker (obj): instance of checker.Checker
• pyrodaemon: Pyro4 daemon sesf.rwlock.servicetester
• serviceparts (obj): read-write-lock serviceparts object
• impproxies: list of Pyro proxies to the implementation.
• lck, cond: lock and condition variable for atomicity of call and return parts.
• awaitend (semaphore): main thread waits here for test to be over.

Functions: j in 0..num_users

• do_acqr(j): do a valid impproxies[j].acqr call and validate return
• do_relr(j): do a valid impproxies[j].relr call and validate return
• do_acqw(j): do a valid impproxies[j].acqw call and validate return
• do_relw(j): do a valid impproxies[j].relw call and validate return
• do_ops(j): issue num_ops read or write (randomly chosen) operations
• do_test(): start do_ops(0), …, do_ops(num_users-1) in separate threads.
• inform_tester(event): RPC-called by implementation to convey event to checker.

Running the servicetester program on an implementation program

Module rwlock.test_imp: has class TestImp that implements an RPC wrapper for any implementation of the read-write-lock service. It redirects incoming RPC calls (from the rwlock servicetester) to regular calls to a rwlock implementation. Run python testimp.py imp_0.imp in a shell to start a TestImp object wrapping the implementation imp_0.imp.Imp.

class rwlock.test_imp.TestImp(use)

Wrap the read-write-lock implementation in parameter use for remote testing. Assume a Pyro4 nameserver is running. Start a Pyro4 daemon and register it as sesf.rwlock.test_imp in a new thread. When function start_testimp is called (by the servicetester), get a proxy for the servicetester and pass it to the implementation (so the implementation can, optionally, inform the servicetester of internal events). After that, pass every incoming call to the implementation until end_pyrodaemon is called. Maintains the following variables:

• use: name of the module whose implementation is to be tested
• imp: Imp object to be tested
• pyrodaemon: Pyro4 daemon rwlock_imp.
• imp.testerproxy: servicetester proxy.

Functions (all RPC-called by servicetester):

• start_testimp(): get proxy for pyrodaemon sesf.rwlock.servicetester (servicetester) and store it in imp.testerproxy.
• acqr(): wrapper for imp.acqr()
• relr(): wrapper for imp.relr()
• acqw(): wrapper for imp.acqw()
• relw(): wrapper for imp.relw()
• end_pyrodaemon(): shutdown local pyrodaemon

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.

1. Start a Pyro4 nameserver if one is not already running: run python -m Pyro4.naming (or python -m Pyro4.naming &).

2. 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).

3. Start the servicetester program: run python servicetester.py <num_threads> <num_ops>

   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 <num_threads> <num_ops> --checker imp_0.checker

Candidate implementation Imp_1

Module rwlock.imp_1.imp has class Imp that implements the read-write-lock service. To instantiate and drive Imp from rwlock/user.py, in the parent directory run “python user.py <num_threads> <num_ops> imp_1.imp <mri>”. Or instantiate Imp in your own program and drive it from there.

class rwlock.imp_1.imp.Imp(argv)

An implementation of the read-write-lock service. Ensures writers do not starve by limiting a “read interval” to at most mri reads, where mri is an initialization argument. (A “read” interval starts when nr becomes non-zero and ends when nr becomes zero.) Imp has functions acqw(), relr(), acqw() and relw(). It maintains the following variables:

• mri (constant int): max number of reads in a “read” interval; set to __init__ parameter mri.
• nr (int): number of threads holding a read lock; initially 0.
• nw (int): number of threads holding a write lock; initially 0.
• nx (int): number of reads started in current interval; initially 0.
• lck (lock): protects nr and nw.
• cvr (condition): to wait for nw == 0 and nx < max_nx
• cvw (condition): to wait for nr and nw equal to 0.

When a thread executes acqw(), it waits on cvw until nr and nw are both 0, then increments nw and returns. At this point, no thread can acquire a write lock or a read lock. When a thread executes relw(), it decrements nw and returns.

When a thread executes acqr(), it waits on cvr until nw == 0 and nx < mri hold, then increments nr and nx, and returns. At this point a thread cannot get a write lock, and can get a read lock only if nx < mri holds. When a thread executes relr(), it decrements nr and, if nr has become zero, zeros nx.

Candidate implementation Imp_2

Module rwlock.imp_2.imp has class Imp that implements the read-write-lock service except that it allows writes to starve. To instantiate and drive Imp from rwlock/user.py, in the parent directory run “python user.py <num_threads> <num_ops> imp_2.imp”. Or instantiate Imp in your own program and drive it from there.

This implementation is of historical interest. It’s one of the earliest solutions and is the one typically presented in texts. It uses sempahores in a “odd” way (locks and condition variables were not invented yet).

class rwlock.imp_2.imp.Imp

An implementation of the read-write-lock service except that it allows writers to starve if there is a continuous supply of readers. It has four functions: acqw(), relr(), acqw() and relw(). It maintains the following variables:

• nr (int): number of threads holding the read lock; initially 0.
• nr_mutex (semaphore): protects nr; “count” initially 1.
• rw_mutex (semaphore): protects a read or write interval; “count” initially 1.

When rw_mutex is free (ie, its count is 1), no thread holds a read lock, no thread holds a write lock, and nr is 0.

When a thread executes acqw(), it acquires rw_mutex. When it executes relw(), it releases rw_mutex. Until then, no other thread can acquire a write lock or a read lock (because rw_mutex is not free).

When a thread executes acqr(), if nr is 0 it acquires rw_mutex and increments nr. At this point no thread can get a write lock. But another thread can get a read lock, because when it executes acqr() it would find nr > 0 and so would not attempt to acquire rw_mutex). When a thread executes relr(), it decrements nr and, if nr is 0 it releases rw_mutex.