% W.H. Hesselink, 11th July 2003. Last modification 22 September 2006

% Mutual exclusion with one binary semaphore
% int sema = 1 ;
% proctype user (int p) {
% 10   do
%      :: break
%      :: skip
% 11      P(sema)
% 12      V(sema)
%      od
% 13

semaMX [Nproc: nat]: THEORY
BEGIN

  state: TYPE = [#
    % global variables
    sema: nat ,
    % private variable
    pc: [below[Nproc] -> nat] 
  #]

  p, q, r: VAR below[Nproc]
  x, y: VAR state 

  step10 (p, x, y): bool =
      x`pc(p) = 10 AND
      (y = x WITH [`pc(p) := 11] OR y = x WITH [`pc(p) := 13])

  step11 (p, x, y): bool =
      x`pc(p) = 11 AND x`sema > 0 AND
      y = x WITH [
          `sema := x`sema - 1 ,
          `pc(p) := 12 ]

  step12 (p, x, y): bool =
      x`pc(p) = 12 AND 
      y = x WITH [
          `sema := x`sema + 1 ,
          `pc(p) := 10 ]

  step (p, x, y): bool =
      step10 (p, x, y) OR step11 (p, x, y) OR step12 (p, x, y)

  init: state =
      (# sema := 1, pc := (LAMBDA (p): 10) #)

% Proof obligations:
% all executions starting in init preserve the invariants
% mutual exclusion, binary semaphore
% (iq0)    q at 12 AND r at 12 IMPLIES q = r
% (iq2)    sema <= 1
% We need the auxiliary invariant 
% (iq1)    q at 12 IMPLIES sema = 0
% In order also to prove absence of deadlock, we need 
% (iq3)    sema = 0 IMPLIES (EXISTS q at 12)

  iq0(q, r, x): bool =
      x`pc(q) = 12 AND x`pc(r) = 12 IMPLIES q = r

  iq1(q, x): bool =
      x`pc(q) = 12 IMPLIES x`sema = 0

  iq2(x): bool =
      (x`sema <= 1)

  iq0_list: LEMMA 
      iq0(q, r, x) AND step(p, x, y) IMPLIES iq0(q, r, y) OR step11(p, x, y)

  iq0_11: LEMMA 
      iq0(q, r, x) AND iq1(q, x) AND iq1(r, x) 
      AND step11(p, x, y) IMPLIES iq0(q, r, y)

  iq0_kept_valid: LEMMA 
      iq0(q, r, x) AND iq1(q, x) AND iq1(r, x) 
      AND step(p, x, y) IMPLIES iq0(q, r, y)

  iq1_list: LEMMA 
      iq1(q, x) AND step(p,x,y) 
      IMPLIES iq1(q, y) OR step11(p, x, y) OR step12(p, x, y)

  iq1_11: LEMMA 
      iq1(q, x) AND iq2(x) AND step11(p,x,y) 
      IMPLIES iq1(q, y)

  iq1_12: LEMMA 
      iq1(q, x) AND iq0(p, q, x) 
      AND step12(p,x,y) IMPLIES iq1(q, y)

  iq1_kept_valid: LEMMA 
      iq1(q, x) AND iq0(p, q, x) AND iq2(x) 
      AND step(p,x,y) IMPLIES iq1(q, y)

  iq2_list: LEMMA 
      iq2(x) AND step(p, x, y) IMPLIES iq2(y) OR step12(p, x, y)

  iq2_12: LEMMA 
      iq2(x) AND iq1(p, x) AND step12(p, x, y) IMPLIES iq2(y)

  iq2_kept_valid: LEMMA 
      iq2(x) AND iq1(p, x) AND step(p,x,y) IMPLIES iq2(y) 

  iq3 (x): bool =
      (x`sema = 0 IMPLIES EXISTS (q): x`pc(q) = 12)

  iq4 (q, x): bool =
      10 <= x`pc(q) AND x`pc(q) <= 13 

  iq3_kept_valid: LEMMA 
      iq3(x) AND step(p,x,y) IMPLIES iq3(y) 

  iq4_kept_valid: LEMMA 
      iq4(q, x) AND step(p, x, y) IMPLIES iq4(q, y) 

  iqall (x): bool = 
      (FORALL q, r: iq0(q, r, x)) AND 
      (FORALL q: iq1(q, x) AND iq4(q, x)) AND iq2(x) AND iq3(x)

  iqall_kept_valid: THEOREM 
      iqall(x) AND step(p,x,y) IMPLIES iqall(y) 

  iqall_holds_initially: THEOREM
      iqall (init)

  hasNext (x): bool =
      (EXISTS (q, y): step (q, x, y))

  terminated (x): bool =
      (FORALL (q): x`pc(q) = 13)

  no_deadlock: THEOREM
      iqall (x) IMPLIES hasNext (x) OR terminated (x)

END semaMX