------------------------------- MODULE IPOFifo -------------------------------
(***************************************************************************)
(* This module defines the abstract program IPOFifo described in Section   *)
(* 7.6.2 of the book "A Science of Concurrent Programs" by Leslie Lamport. *)
(* It is instantiated by the module IPOFifo_pqs.                           *)
(***************************************************************************)

(***************************************************************************)
(* The constants are the same as for the abstract program Fifo of Section  *)
(* 7.6.1 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.                   *)
  (*************************************************************************)
  
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 16:12:55 CEST 2024 by lamport
\* Created Thu Sep 15 07:19:08 PDT 2022 by lamport
