------------------------------- MODULE IPOFifo -------------------------------
(***************************************************************************)
(* This is another specification of a linearizable queue that is           *)
(* equivalent to that of Fifo, where PO stands for NonDeterministic.  It   *)
(* has the same interface variables eqn and deq.  However, instead of      *)
(* maintaining a totally ordered queue of enqueued data items, it          *)
(* maintains a set of elts of enqueued elements partially ordered by a     *)
(* relation \prec, where d1 \prec d2 means that data item d1 must be       *)
(* dequeued before data item d2.  This relation is defined by d1 \prec d2  *)
(* iff the EndDeq action for d1 precedes the BeginDeq action for d2.       *)
(*                                                                         *)
(* The obvious way to write a linearizable specification is to have        *)
(* internal DoEnqueue and DoDequeue actions that add and remove the        *)
(* enqueued value to/from elts.  However, it doesn't matter in what order  *)
(* DoEnqueue of two overlapping Enqueue operations are performed, because  *)
(* neither of the two values they add to elts precedes the other in the    *)
(* \prec relation.  This implies that we can simplify the nondeterministic *)
(* Fifo spec by eliminating the DoEnqueue action and having the            *)
(* BeginEnqueue action add the element to elts.  Similarly, we can         *)
(* eliminate the DoDequeue action and have the EndDequeue action remove    *)
(* the element being dequeued from elts.  The unsimplified and simplified  *)
(* versions of the nondeterministic Fifo queue are equivalent when we hide *)
(* all internal variables--that is, all variables other than the interface *)
(* variables enq and deq.                                                  *)
(*                                                                         *)
(* The \prec order is therefore implemented by having the BeginEnqueue     *)
(* action that adds the element d to the set of enqueued values also add a *)
(* relation d \prec e for every enqueued element e for which the           *)
(* EndEnqueue operation has already been executed.  A Dequeue operation    *)
(* can dequeue any element d for which d \prec e equals FALSE for every    *)
(* other enqueued value e.                                                 *)
(*                                                                         *)
(* Multiple copies of the same data item can be in the queue at the same   *)
(* time, and we have to be able to distinguish them.  What the abstract    *)
(* program POFifo does is to maintain a set elts of pairs <<d,i>>, where d *)
(* is the data value and i is an element in a set Ids of identifiers.      *)
(* When a data item d is enqueued, the value <<d,i>> is added to the set   *)
(* elts for some identifier i for which <<d,i>> is not in elts.  A         *)
(* <<Data,Ids>> pair is called an element.                                 *)
(***************************************************************************)

\* Note that no modules are being EXTENDed

(***************************************************************************)
(* The constants are the same as for Fifo, except for Ids, which is an     *)
(* arbitrary set of identifiers.  (The constant NoData is not needed.)     *)
(***************************************************************************)
CONSTANTS EnQers, DeQers, Data, Busy, Done, Ids  

ASSUME /\ Done \notin Data
       /\ Busy \notin Data

Datums ==  Data \X Ids
  (*************************************************************************)
  (* The set of all values that can be enqueued in elts.  It is used only  *)
  (* in type-correctness invariants.                                       *)
  (*************************************************************************)
  
NonElt == << >>
  (*************************************************************************)
  (* We could let NonElt be any value not in Datums; this is a simple    *)
  (* choice.                                                               *)
  (*************************************************************************)  

(***************************************************************************)
(* THE VARIABLES:                                                          *)
(*   enq, deq : The same interface variables as Fifo.                      *)
(*                                                                         *)
(*   elts : The set of elements currently enqueued.                        *)
(*                                                                         *)
(*   before : The relation \prec on a set elts is defined the way          *)
(*            mathematicians generally define a relation on a set:         *)
(*            as a subset of elts \X elts, where d \prec e is              *)
(*            defined to mean <<d, e>> is in that set.  The value of       *)
(*            `before' is the set that defines the \prec relation on       *)
(*            the set elts.                                                *)
(*                                                                         *)
(*   adding[e] : If enqueuer e is performing an Enqueue operation, then    *)
(*               this is the element it has put in elts.  Otherwise, it    *)
(*               equals NonElt.                                      *)
(***************************************************************************)
VARIABLES enq, deq, elts, before, adding
POv == <<enq, deq, elts, before, adding>>

e1 \prec e2 == <<e1, e2>> \in before

POTypeOK == /\ enq \in [EnQers -> Data \cup {Done}]
            /\ deq \in [DeQers -> Data \cup {Busy}]
            /\ elts \in SUBSET Datums
            /\ before \in SUBSET (elts \X elts)
            /\ adding \in [EnQers -> Datums \cup {NonElt}]

POInit == /\ enq = [e \in EnQers |-> Done]
          /\ elts  = {}
          /\ deq \in [DeQers -> Data]
          /\ before = {}
          /\ adding = [e \in EnQers |-> NonElt]
-----------------------------------------------------------------------------
(***************************************************************************)
(* beingAdded is essentially the set of of elements being enqueued by an   *)
(* Enqueue operation that has not completed.                               *)
(***************************************************************************)
beingAdded == {adding[e] : e \in EnQers} \ {NonElt}

(***************************************************************************)
(* THE ACTIONS:                                                            *)
(* We add the PO to the names of the Begin and End actions to avoid name   *)
(* clashes with the Fifo abstract program.                                 *)
(***************************************************************************)     
 
(***************************************************************************)
(* The BeginPOEnq(e) action for enqueuer e adds an element to elts and     *)
(* updates the \prec relation (by changing `before').  It enqueues an      *)
(* arbitrary data item D, giving it an id such that <<D, id>> is not in    *)
(* elts or in beingAdded.  We can't have the action add to elts an element *)
(* that that equals adding[e2] for an enqueuer e2 # e even if that element *)
(* has been removed from elts by a Dequeue operation, because beingAdded   *)
(* is used in updating the \prec relation, and that could cause incorrect  *)
(* \prec relations to be added.  The action also sets adding[e].           *)
(***************************************************************************)
BeginPOEnq(e) ==
  /\ enq[e] = Done 
  /\ \E D \in Data : 
       \E id \in {i \in Ids : <<D, i>> \notin (elts \cup beingAdded)} :
         /\ enq' = [enq EXCEPT ![e] =  D]
         /\ elts' = elts \cup {<<D, id>>} 
         /\ before' = before \cup {<<el, <<D, id>>>> : el \in (elts \ beingAdded)}
         /\ adding' = [adding EXCEPT ![e] = <<D, id>>]
  /\  deq' = deq

(***************************************************************************)
(* The EndPOEnq(e) and BeginNdDeq(d) for an enqueuer e and a dequeuer d do *)
(* the obvious things.                                                     *)
(***************************************************************************)                           
EndPOEnq(e) == /\ enq[e] # Done
               /\ enq' = [enq EXCEPT ![e] =  Done]
               /\ adding' = [adding EXCEPT ![e] =  NonElt]
               /\ UNCHANGED <<deq, elts, before>>

BeginPODeq(d) == /\ deq[d] # Busy
                 /\ deq' = [deq EXCEPT ![d] =  Busy]
                 /\ UNCHANGED <<enq, elts, before, adding>>

(***************************************************************************)
(*  The EndPODeq(d) action removes from elts an arbitrary element el       *)
(*  that is no preceded in the \prec relationby any other element in elts. *)
(*  Remember that el[1] is the data item contained in the element el.      *)
(***************************************************************************)               
EndPODeq(d) == /\ deq[d] = Busy
               /\ \E el \in elts :
                    /\ \A el2 \in elts : ~(el2 \prec el)
                    /\ elts' = elts \ {el}
                    /\ deq' = [deq EXCEPT ![d] =  el[1]]
                    /\ before' = before \cap (elts' \X elts')
               /\ UNCHANGED <<enq, adding>>
             
PONext == \/ \E e \in EnQers : BeginPOEnq(e)  \/ EndPOEnq(e)
          \/ \E d \in DeQers : BeginPODeq(d)  \/ EndPODeq(d)
 
POFifo == POInit /\ [][PONext]_POv
=============================================================================
\* Modification History
\* Last modified Sat Oct 19 12:29:13 CEST 2024 by lamport
\* Created Thu Sep 15 07:19:08 PDT 2022 by lamport
