--
-- Mutual Exclusion Algorithm using test&set.
--
--
-- We want at most one process to enter a section where shared resources are
-- accessed at the same time. The section is called the critical section.
-- We write a program called MUTEX that achieves this purpose using test&set.
-- test&set stores some value in a variable and returns the old value of 
-- the variable atomically, indivisibly, or without any intervention.
--
-- What test&set does can be described as follows, although it perfomrs this
-- atomically:
--
--   Boolean test&set(Boolean x, Boolean *y) {
--     /* do the following atomically */
--     Boolean t = *y;
--     *y = x;
--     return t;
--   }
--
-- Program MUTEX uses one boolean variable that is defined as follows:
--
--   Boolean locked = false;
--
-- locked is shared by all processes, initially set to false. 
--
-- Then program MUTEX executed by process i is defined as follows:
--
--   l1: if (test&set(true,&locked)) goto l1;
--   cs: Critical Section
--   l2: locked = false;
--
-- Process i is supposed to execute this program repeatedly.
-- In Critical Section, process i accesses the shared resources.
--
-- You may be convinced that this program achieves the purpose. 
-- But can you explain why it does rigorously?
--
-- We can do by writing proof scores in CafeOBJ. Before that, however,
-- we have to make a formal model of the program. Formal models used are
-- a kind of transition system, called OTS's (observational transition systems).
-- 
-- The formal model of the program:
--   - Three transition rules are used.
--     * 'begin_i' corresponds to 'if (test&set(true,&locked)) goto l1'.
--     * 'exit_i'  corresponds to 'Critical Section'.
--     * 'end_i'   corresponds to 'locked = false'.
--   - Two variables (observable values) are used.
--     * 'locked' denotes variable locked.
--     * 'pc_i'   indicates where process i is at.
--
-- Transition rules have conditions on which they are effectively executed.
-- The conditions are called effective conditions of the transition rules.
-- The effective condition of transition rule 'tr' is denoted by 'c-tr'.
--
-- The effective conditions:
--   - c-begin_i : pc_i = l1 and not(locked)
--   - c-exit_i  : pc_i = cs
--   - c-end_i   : pc_i = l2
--
-- The definitions of the transition rules can be written as follows:
--   - begin_i : if c-begin_i then
--                 locked := true;
--                 pc_i   := cs;
--                 any other values are not changed
--               else
--                 any values are not changed
--               fi
--
--   - exit_i  : if c-exit_i then
--                 pc_i := l2;
--                 any other values are not changed
--               else
--                 any values are not changed
--               fi
--
--   - end_i   : if c-exit_i then
--                 lcoked := false;
--                 pc_i   := l1;
--                 any other values are not changed
--               else
--                 any values are not changed
--               fi
--
-- The formal model is described in CafeOBJ.
--
-- In the formal model, we use two kinds of data types: process IDs and labels
-- (l1,cs,l2), which are defined in module Process and module LABEL.
--

--
-- Operator _=_ is the equality predicate of Process as you can imagine.
-- CafeOBJ provides built-in equality predicate _==_.
--
-- *** This part MAY be skipped. ***
-- Given two terms t1 and t2, 't1 == t2' is true if the results of reducing
-- the two terms are the same, and otherwise it is false.
-- If the CafeOBJ specification regarded as a TRS is confluent, it is safe to
-- use _==_. Otherwise you should use it carefully. _==_ may decides two possible 
-- equal temrs are different.
-- 
-- Besides, if you use _==_, you may write proof scores more than using _=_.
-- Supose that two constants c1 and c2 are declared in a proof score.
-- If you use _==_, the two constants are treated as different objects.
-- Therefore, we should write a proof score for another case where the two 
-- constants are eqaul.
-- If you use _=_, the two constants are treated as completely arbitrary objects,
-- they may be eqaul or may be different, provided that no constraints on 
-- the constants are given.
-- ************************************
--
-- We can use 'comm' to make an operator commutative, namely that
-- (t1 = t2) equals (t2 = t1).
--
mod* PROCESS {
  [Process]
  op _=_ : Process Process -> Bool {comm}
  var P : Process
  eq (P = P) = true .
}

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

--
-- The formal model is described in module MUTEX.
--
--   - Hidden sort 'System' denotes the state space.
--   - Constant    'init'   denotes any initial state.
--   - Operator    'locked' denotes variable locked.
--   - Operator    'pc'     denotes pc_i, 
--       more precisely, term 'pc(s,i)' denotes pc_i in state s.
--   - Operator    'begin'  denotes transition rule begin_i,
--       more precisely, term 'begin(s,i)' denotes the successor state after
--       executing begin_i in state s.
--   - Operator    'exit'   denotes transition rule exit_i.
--   - Operator    'end'    denotes transition rule end_i.
--
--   - Operator     'c-begin' denotes the effective condition of begin_i.
--   - Operator     'c-exit'  denotes the effective condition of exit_i.
--   - Operator     'c-end'   denotes the effective condition of end_i.
--
mod* MUTEX {
  pr(PROCESS + LABEL)
  *[System]*
-- any initial state
  op init : -> System
-- observations
  bop locked : System -> Bool
  bop pc     : System Process -> Label
-- actions
  bop begin : 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 and not locked(S)) .
  --
  ceq locked(begin(S,P)) = true if c-begin(S,P) .
  ceq pc(begin(S,P),Q)   = (if (P = Q) then cs else pc(S,Q) fi) 
      if c-begin(S,P) .
  ceq begin(S,P)         = S    if not c-begin(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) .
  ceq pc(exit(S,P),Q)   = (if (P = Q) then l2 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) = l2) .
  --
  ceq locked(end(S,P)) = false if c-end(S,P) .
  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) .
}