--
-- A mutual exclusion algorithm using atomicSwap.
--
-- We want at most one process to enter a section where shared
-- resources are accessed, called the critical section, at the same
-- time. We write a program that achieves this purpose using
-- atomicSwap. atomicSwap exchanges the contents of two variables
-- atomically, which is defined as follows:
--
--   void atomicSwap(Boolean *x, Boolean *y) {
--     /* do the following atomically */
--     int t = *x; 
--     *x = *y;
--     *y = t;
--   }
--
-- The program uses two variables that are defined as follows:
-- 
--   Boolean locked = false;
--   Boolean check[N]; /* N is the number of processes. */
--
-- locked is shared by all processes, initially set to false. check[i]
-- is only accessed by process i. 
--
-- Then, the program executed by process i is defined as follows:
--   
--   l1: check[i] = true;
--   l2: atomicSwap(&check[i], &locked);
--   l3: if (check) goto l2;
--   cs: Critical Section;
--   l4: locked = false;
--
-- Process i is supposed to execute this program repeatedly.
--
-- But, does this program achieves the purpose? That is, does the
-- program allow at most one process to enter the critical section at
-- the same time? If you think so, why?
--
-- One way of convincing you that the program achieves the purpose is
-- to verify it formally. Before that, however, we have to make the
-- formal (mathematical) model of the program.
--
-- We use OTS's (observational transition systems), a kind of
-- transition system, for the formal model of the program. OTS's are
-- described in CafeOBJ. First we describe data types used in the
-- program in CafeOBJ.
--

mod* PROCESS {
  [Process]
  op _=_ : Process Process -> Bool {comm}
  var P : Process
  eq (P = P) = true .
}

mod! LABEL {
  [Label]
  ops l1 l2 l3 cs l4 : -> Label
  op _=_ : Label Label -> Bool {comm}
  var L : Label
  eq (L = L) = true .
  eq (l1 = l2) = false .
  eq (l1 = l3) = false .
  eq (l1 = cs) = false .
  eq (l1 = l4) = false .
  eq (l2 = l3) = false .
  eq (l2 = cs) = false .
  eq (l2 = l4) = false .
  eq (l3 = cs) = false .
  eq (l3 = l4) = false .
  eq (cs = l4) = false .
}

-- 
-- Next we describe the OTS modeling the program in CafeOBJ.
--

mod* MUTEX {
  pr(PROCESS + LABEL)
  *[System]*
-- any initial state
  op init : -> System
-- observations
  bop locked : System -> Bool
  bop check  : System Process -> Bool
  bop pc     : System Process -> Label
-- actions
  bop begin : System Process -> System
  bop swap  : System Process -> System
  bop test  : System Process -> System
  bop exit  : System Process -> System
  bop end   : System Process -> System
-- CafeOBJ variables
  var S : System
  vars P Q : Process
-- for any initial state
  eq locked(init) = false .
  eq pc(init,P) = l1 .
-- begin
  op c-begin : System Process -> Bool {strat: (0 1 2)}
  eq c-begin(S,P) = (pc(S,P) = l1) .
  --
  eq  locked(begin(S,P))  = locked(S) .
  ceq check(begin(S,P),Q) = (if (P = Q) then true else check(S,Q) fi)
      if c-begin(S,P) .
  ceq pc(begin(S,P),Q)    = (if (P = Q) then l2 else pc(S,Q) fi)
      if c-begin(S,P) .
  ceq begin(S,P)          = S if not c-begin(S,P) .
-- swap
  op c-swap : System Process -> Bool {strat: (0 1 2)}
  eq c-swap(S,P) = (pc(S,P) = l2) .
  --
  ceq locked(swap(S,P))  = check(S,P) if c-swap(S,P) .
  ceq check(swap(S,P),Q) = (if (P = Q) then locked(S) else check(S,Q) fi)
      if c-swap(S,P) .
  ceq pc(swap(S,P),Q)    = (if (P = Q) then l3 else pc(S,Q) fi)
      if c-swap(S,P) .
  ceq swap(S,P)          = S if not c-swap(S,P) .
-- test
  op c-test : System Process -> Bool {strat: (0 1 2)}
  eq c-test(S,P) = (pc(S,P) = l3) .
  --
  eq  locked(test(S,P))  = locked(S) .
  eq  check(test(S,P),Q) = check(S,Q) .
  ceq pc(test(S,P),Q)    
      = (if (P = Q) then (if check(S,Q) then l2 else cs fi) else pc(S,Q) fi)
      if c-test(S,P) .
  ceq test(S,P)          = S if not c-test(S,P) .
-- exit
  op c-exit : System Process -> Bool {strat: (0 1 2)}
  eq c-exit(S,P) = (pc(S,P) = cs) .
  --
  eq  locked(exit(S,P))  = locked(S) .
  eq  check(exit(S,P),Q) = check(S,Q) .
  ceq pc(exit(S,P),Q)    = (if (P = Q) then l4 else pc(S,Q) fi) if c-exit(S,P) .
  ceq exit(S,P)          = S if not c-exit(S,P) .
-- end
  op c-end : System Process -> Bool {strat: (0 1 2)}
  eq c-end(S,P) = (pc(S,P) = l4) .
  --
  ceq locked(end(S,P))  = false if c-end(S,P) .
  eq  check(end(S,P),Q) = check(S,Q) .
  ceq pc(end(S,P),Q)    = (if (P = Q) then l1 else pc(S,Q) fi) if c-end(S,P) .
  ceq end(S,P)          = S if not c-end(S,P) .
}