(*---------------------------------------------------------------------------*)
(* IA64 memory model in HOL4                                                 *)
(*                                                                           *)
(* Originally written by Konrad Slind - slind@cs.utah.edu                    *)
(*                                                                           *)
(* Based on specification by Yue Yang for his PhD work                       *)
(* See www.cs.utah.edu/~yyang/publications.html                              *)
(*                                                                           *)
(* Yang's specification was based on Intel's Formal Spec                     *)
(*                                                                           *)
(* Intel's document is the first entry listed by Google if you search for    *)
(* 25142901.pdf :-)                                                          *)
(*                                                                           *)
(* Comments added by Ganesh (ganesh@cs.utah.edu)                             *)
(* Also one fix added by Ganesh based on Ali Sezgin's proof-reading          *)
(*                                                                           *)
(* Only use so far: Looked at this HOL description to code up the program    *)
(* that was reported in our CAV'04 paper (Gopalakrishnan, Yang, Sivaraj      *)
(* "QB or not QB: ..." available from Yang's website above                   *)
(*                                                                           *)
(* First load some theories required by the spec.                            *)
(*---------------------------------------------------------------------------*)

app load ["integerTheory", "pred_setTheory"];
val _ = numLib.prefer_num();

(*---------------------------------------------------------------------------*)
(* Kinds of instruction: load-acquire, store-release, unordered load,        *)
(*                       unordered store, and memory fence                   *)
(*---------------------------------------------------------------------------*)

Hol_datatype `ikind = LdAcq | StRel | Ld | St | Mf`;

(*---------------------------------------------------------------------------*)
(* Type of a write operation                                                 *)
(*---------------------------------------------------------------------------*)

Hol_datatype `wtype = Local | Remote`;

(*---------------------------------------------------------------------------*)
(* Memory locations are modelled with an (address,attribute,default) triple  *)
(* Attributes of memory locations can be : write-back, uncacheable, or       *)
(*                                         write-coalescing                  *)
(*---------------------------------------------------------------------------*)

Hol_datatype `attr = WB | UC | WC`;

val attr_of_def    = Define `attr_of    (address,attr,default) = attr`;
val default_of_def = Define `default_of (address,attr,default) = default`;

(*---------------------------------------------------------------------------*)
(* Memory operations                                                         *)
(*---------------------------------------------------------------------------*)

val _ = Hol_datatype
        `instr = <| proc : num ;       (* issuing process *)
                    id   : num ;       (* global id *)
                    pc   : num ;       (* program counter *)
		    op   : ikind ;     (* operation *)
                    var  : num # attr # int; (* address, attribute, default *)
                    data : int ;       (* data for a write *)
                    wrID : num ;       (* id of a write operation *)
                  wrType : wtype ;     (* is a write local or remote? *)
                  wrProc : num ;       (* target process of a write *)
                     reg : num ;       (* register *)
                  useReg : bool        (* does write use a reg? *)
                   |>`;

(*---------------------------------------------------------------------------*)
(*   Predicates on whether an instruction is a read or write                 *)
(*---------------------------------------------------------------------------*)

val isWr_def = Define `isWr i = (i.op = StRel) \/ (i.op = St)`;

val isRd_def = Define `isRd i = (i.op = LdAcq) \/ (i.op = Ld)`;

(*---------------------------------------------------------------------------*)
(*       requireLinearOrder                                                  *)
(*       Ganesh now calls it strictTotalOrder as is more traditional imho    *)
(*---------------------------------------------------------------------------*)
val requireIrreflexive_def = Define
   `requireIrreflexive ops order =
           !i j. i IN ops /\ j IN ops /\ (i.id = j.id) ==> ~order i j`;

val requireTransitive_def = Define
   `requireTransitive ops order =
           !i j k. i IN ops /\ j IN ops /\ k IN ops ==>
                   order i j /\ order j k ==> order i k`;

val requireTotal_def = Define
   `requireTotal ops order =
           !i j. i IN ops /\ j IN ops /\ ~(i.id = j.id)
                 ==> order i j \/ order j i`;

(*...........................................................................*)
(* This was in our original definition - but is redundant                    *)
(*...........................................................................*)
val requireCircuitFree_def = Define
   `requireCircuitFree ops order =
           !i j. i IN ops /\ j IN ops ==> order i j ==> ~order j i`;

val requireStrictTotalOrder_def = Define
   `requireStrictTotalOrder ops order = requireIrreflexive ops order /\
                                        requireTransitive ops order  /\
                                        requireTotal ops order`;


(*---------------------------------------------------------------------------*)
(*       requireWriteOperationOrder                                          *)
(*---------------------------------------------------------------------------*)

val orderedByWriteOperation_def = Define
   `orderedByWriteOperation i j =
         isWr i /\ isWr j /\ (i.wrID = j.wrID) /\
         ((i.wrType = Local) /\ (j.wrType = Remote) /\
          (j.wrProc = i.proc)
         \/
          (i.wrType = Remote) /\ (j.wrType = Remote) /\
          (i.wrProc = i.proc) /\ ~(j.wrProc = i.proc))`;

val requireWriteOperationOrder_def = Define
   `requireWriteOperationOrder ops order =
           !i j. i IN ops /\ j IN ops /\ orderedByWriteOperation i j
                 ==> order i j`;

(*---------------------------------------------------------------------------*)
(*       requireProgramOrder                                                 *)
(*---------------------------------------------------------------------------*)

val orderedByProgram_def = Define
   `orderedByProgram i j = (i.proc = j.proc) /\ i.pc < j.pc`;

val orderedByAcquire_def = Define
   `orderedByAcquire i j = orderedByProgram i j /\ (i.op = LdAcq)`;

val orderedByFence_def = Define
   `orderedByFence i j = orderedByProgram i j /\ ((i.op = Mf) \/ (j.op = Mf))`;

val orderedByRelease_def = Define
   `orderedByRelease i j =
      orderedByProgram i j /\ (j.op = StRel) /\
      (isWr i ==>
          (i.wrType = Local) /\ (j.wrType = Local) \/
          (i.wrType=Remote) /\ (j.wrType=Remote) /\ (i.wrProc=j.wrProc))`;

val requireProgramOrder_def = Define
   `requireProgramOrder ops order =
           !i j. i IN ops /\ j IN ops ==>
                 orderedByAcquire i j \/
                 orderedByRelease i j \/
                 orderedByFence i j
                    ==>
                 order i j`;

(*---------------------------------------------------------------------------*)
(*       requireMemoryDataDependence                                         *)
(*---------------------------------------------------------------------------*)

val orderedByMemoryData_def = Define
   `orderedByMemoryData i j = orderedByProgram i j /\ (i.var = j.var)`;

val orderedByRAW_def = Define
   `orderedByRAW i j = orderedByMemoryData i j /\
                       isWr i /\ isRd j /\ (i.wrType = Local)`;

val orderedByWAR_def = Define
   `orderedByWAR i j = orderedByMemoryData i j /\
                       isRd i /\ isWr j /\ (j.wrType = Local)`;


val orderedByWAW_def = Define
   `orderedByWAW i j = orderedByMemoryData i j /\
                       isWr i /\ isWr j /\
                       ((i.wrType = Local) /\ (j.wrType = Local)
                          \/
                        (i.wrType = Remote) /\ (j.wrType = Remote)
                                            /\ (i.wrProc = i.proc)
                                            /\ (j.wrProc = i.proc))`;

val requireMemoryDataDependence_def = Define
   `requireMemoryDataDependence ops order =
           !i j. i IN ops /\ j IN ops ==>
                 (orderedByRAW i j \/ orderedByWAR i j \/ orderedByWAW i j)
                 ==>
                  order i j`;

(*---------------------------------------------------------------------------*)
(*       requireDataFlowDependence                                           *)
(*---------------------------------------------------------------------------*)

val orderedByLocalDependence_def = Define
   `orderedByLocalDependence i j =
         orderedByProgram i j /\ (i.reg = j.reg) /\
         ((isRd i /\ isRd j)                                   \/
          (isWr i /\ isRd j /\ (i.wrType = Local) /\ i.useReg) \/
          (isRd i /\ isWr j /\ (j.wrType = Local) /\ j.useReg) \/
          (isWr i /\ isWr j /\ (i.wrType = Local) /\ (j.wrType = Local)
                            /\ i.useReg /\ j.useReg))`;


val requireDataFlowDependence_def = Define
   `requireDataFlowDependence ops order =
           !i j. i IN ops /\ j IN ops ==>
                 orderedByLocalDependence i j ==> order i j`;

(*---------------------------------------------------------------------------*)
(*       requireCoherence                                                    *)
(*---------------------------------------------------------------------------*)

val requireCoherence_def = Define
   `requireCoherence ops order =
        !i j. i IN ops /\ j IN ops
              ==> isWr i /\ isWr j /\ (i.var = j.var) /\ order i j /\
               ((attr_of i.var = WB) \/ (attr_of i.var = UC)) /\
               ((i.wrType=Local) /\ (j.wrType=Local) /\ (i.proc=j.proc)
                  \/
                (i.wrType=Remote) /\ (j.wrType=Remote) /\ (i.wrProc=j.wrProc))
              ==>
                !p q. p IN ops /\ q IN ops ==>
                      isWr p /\ isWr q /\
                      (p.wrID = i.wrID) /\ (q.wrID = j.wrID) /\
                      (p.wrType = Remote) /\ (q.wrType = Remote) /\
                      (p.wrProc = q.wrProc)
                     ==>
                        order p q`;

(*---------------------------------------------------------------------------*)
(*       requireReadValue                                                    *)
(*---------------------------------------------------------------------------*)

val validLocalWr_def = Define
   `validLocalWr ops order j = ?i. i IN ops /\ isWr i /\
                                   (i.wrType = Local) /\
                                   (i.var = j.var)    /\
                                   (i.proc = j.proc)  /\
                                   order i j          /\
                                   (i.data = j.data)
                                   /\
                                   ~?k. k IN ops /\ isWr k /\
                                        (k.wrType = Local) /\
                                        (k.var=j.var)      /\
                                        (k.proc = j.proc)  /\
                                        order i k          /\
                                        order k j`;

val validRemoteWr_def = Define
   `validRemoteWr ops order j = ?i. i IN ops /\ isWr i /\
                                   (i.wrType = Remote) /\
                                   (i.wrProc = j.proc) /\
                                   (i.var = j.var)     /\
                                   ~order j i          /\
                                   (i.data = j.data)
                                   /\
                                   ~?k. k IN ops /\ isWr k  /\
                                        (k.wrType = Remote) /\
                                        (k.var = j.var)     /\
                                        (k.wrProc = j.proc) /\
                                        order i k /\ order k j`;

(**** Variant of above definition of validRemoteWr_def ****
val validRemoteWr_def = Define
   `validRemoteWr ops order j = ?i. i IN ops /\ isWr i /\
                                   (i.wrType = Remote) /\
                                   (i.wrProc = j.proc) /\
                                   (i.var = j.var)     /\
                                   ~order j i          /\
                                   (i.data = j.data)
                                   /\
                                    !k.    !k IN ops
                                        \/ !isWr k
                                        \/ !(k.wrType = Remote)
                                        \/ !(k.var = j.var)    
                                        \/ (k.wrProc = j.proc)
                                        \/ ~order i k
                                        \/ ~order k j`;
********)

val validDefaultWr_def = Define
   `validDefaultWr ops order j = (~?i. i IN ops /\ isWr i /\
                                      (i.var = j.var) /\ order i j /\
                                   ( (i.wrType = Local) /\ (i.proc = j.proc)        (* <- Fixes: added *)
                                     \/                                             (* <- these three *)
                                     (i.wrType = Remote) /\ (i.wrProc = j.proc))    (* <- lines based on Ali's *)
                                 ==>                                                (* proof-reading *)
                                  (j.data = default_of j.var)`;


val validRd_def = Define
   `validRd ops order j = ?i. i IN ops /\ isRd i /\
                              (i.reg = j.reg) /\
                              orderedByProgram i j /\
                              (i.data = j.data) /\
                              ~?k. k IN ops /\ isRd k /\
                                   (k.reg = j.reg) /\
                                   orderedByProgram i k /\
                                   orderedByProgram k j`;

val requireReadValue_def = Define
   `requireReadValue ops order =
        !j. j IN ops ==> (isRd j ==> validLocalWr ops order j \/
                                     validRemoteWr ops order j \/
                                     validDefaultWr ops order j)
                      /\ (isWr j /\ j.useReg ==> validRd ops order j)`;

(*---------------------------------------------------------------------------*)
(*       requireAtomicWBRelease                                              *)
(*---------------------------------------------------------------------------*)

val requireAtomicWBRelease_def = Define
   `requireAtomicWBRelease ops order =
           !i j k. i IN ops /\ j IN ops /\ k IN ops
                   ==>
                    (i.op = StRel) /\ (i.wrType = Remote) /\
                    (k.op = StRel) /\ (k.wrType = Remote) /\
                    (i.wrID = k.wrID) /\
                    (attr_of i.var = WB) /\
                    order i j /\ order j k
                   ==>
                    (j.op = StRel) /\ (j.wrType = Remote) /\
                    (j.wrID = i.wrID)`;

(*---------------------------------------------------------------------------*)
(*       requireSequentialUC                                                 *)
(*---------------------------------------------------------------------------*)

val orderedByUC_def = Define
   `orderedByUC i j =
        orderedByProgram i j /\
        (attr_of i.var = UC) /\
        (attr_of j.var = UC) /\
        (isRd i /\ isRd j                     \/
         isRd i /\ isWr j /\ (j.wrType=Local) \/
         isWr i /\ isRd j /\ (i.wrType=Local) \/
         isWr i /\ isWr j /\ (i.wrType=Local) /\ (j.wrType=Local))`;

val requireSequentialUC_def = Define
   `requireSequentialUC ops order =
           !i j. i IN ops /\ j IN ops /\ orderedByUC i j ==> order i j`;

(*---------------------------------------------------------------------------*)
(*       requireNoUCBypass                                                   *)
(*---------------------------------------------------------------------------*)

val requireNoUCBypass_def = Define
   `requireNoUCBypass ops order =
           !i j k. i IN ops /\ j IN ops /\ k IN ops
                   ==>
                    isWr i /\ isRd j /\ isWr k /\
                    (i.wrType = Local) /\
                    (k.wrType = Remote) /\
                    (k.wrProc = k.proc) /\
                    (k.wrID = i.wrID) /\
                    (attr_of i.var = UC) /\
                    order i j /\
                    order j k
                   ==>
                    ~(k.wrProc = j.proc) \/ ~(i.var = j.var)`;

(*---------------------------------------------------------------------------*)
(* Definition of a legal trace                                               *)
(*---------------------------------------------------------------------------*)

val legal_def = Define
   `legal ops = ?order. requireStrictTotalOrder ops order
                   /\   requireWriteOperationOrder ops order
                   /\   requireProgramOrder ops order
                   /\   requireMemoryDataDependence ops order
                   /\   requireDataFlowDependence ops order
                   /\   requireCoherence ops order
                   /\   requireReadValue ops order
                   /\   requireAtomicWBRelease ops order
                   /\   requireSequentialUC ops order
                   /\   requireNoUCBypass ops order`;

(*---------------------------------------------------------------------------*)