distlock2.service.ppy

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

class Service():
  def __init__(self):
    """Maintains the following variables:
    - acqrd: address at which user holds lock; None if lock is free.
    - ongoing[j]: true iff acq(j), rel(j) or end(j) call ongoing; j in 0..1.
    - ended: true iff end(j) has been called for some j
    """
    self.acqrd = None
    self.ongoing = [False, False]
    self.ended = False

  def acq(self, j):
    CIC:
      j in (0, 1) and not self.ended and not self.ongoing[j]
      and self.acqrd != j
    CU:
      self.ongoing[j] = True

    RETURN():
      ROC:
        self.acqrd == None
      RU:
        self.ongoing[j] = False
        self.acqrd = j
   

  def rel(self, j):
    CIC:
      j in (0, 1) and not self.ended and not self.ongoing[j]
      and self.acqrd == j 
    CU:
      self.ongoing[j] = True
      self.acqrd = None

    RETURN():
      ROC:
        True
      RU:
        self.ongoing[j] = False


  def end(self, j):
    CIC:
      j in (0, 1) and not self.ended and self.acqrd == None
      and not self.ongoing[0] and not self.ongoing[1]
    CU:
      self.ongoing[j] = True
      self.ended = True

    RETURN():
      ROC:
        True
      RU:
        self.ongoing[j] = False