(*        x86-TSO Semantics: HOL sources                                *)
(*                                                                      *)
(* Scott Owens, Susmit Sarkar, Peter Sewell                             *)
(*                                                                      *)
(*  Computer Laboratory, University of Cambridge                        *)
(*                                                                      *)
(*  Copyright 2007-2009                                                 *)
(*                                                                      *)
(* Redistribution and use in source and binary forms, with or without   *)
(* modification, are permitted provided that the following conditions   *)
(* are met:                                                             *)
(*                                                                      *)
(* 1. Redistributions of source code must retain the above copyright    *)
(*    notice, this list of conditions and the following disclaimer.     *)
(* 2. Redistributions in binary form must reproduce the above copyright *)
(*    notice, this list of conditions and the following disclaimer in   *)
(*    the documentation and/or other materials provided with the        *)
(*    distribution.                                                     *)
(* 3. The names of the authors may not be used to endorse or promote    *)
(*    products derived from this software without specific prior        *)
(*    written permission.                                               *)
(*                                                                      *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS   *)
(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED    *)
(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE   *)
(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY      *)
(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL   *)
(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE    *)
(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS        *)
(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,         *)
(* WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING            *)
(* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS   *)
(* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.         *)

(*
use "lts_memory_modelScript.sml";
app load ["axiomatic_memory_modelTheory", "pathTheory", "HolDoc"];
*)


open HolKernel boolLib Parse bossLib wordsTheory;
open combinTheory pathTheory;
open axiomatic_memory_modelTheory;

open HolDoc;

val _ = new_theory "lts_memory_model";

val clause_name_def = Define `clause_name x = T`;

val _ = Hol_datatype `
  machine_state = <|  R : proc -> 'reg -> value option;     (* per-processor registers *)
    M : address -> value option;          (* main memory *)
    B : proc -> (address # value) list;   (* per-processor write buffers *)
    L : proc option                       (* which processor holds the lock *) |>`;


val _ = Define `
  not_blocked s p = (s.L = NONE) \/ (s.L = SOME p)`;

val _ = Define `
  no_pending b a = ~(?v'. MEM (a, v') b)`;

val _ = Hol_datatype `
  label =  Tau | Evt of proc => ('reg action) | Lock of proc | Unlock of proc`;


(* 
The following lts blocks on the global lock for some transitions and not for
others.  We conjecture that all of the commented-out not_blockeds could be added
in to arrive at a stricter, but observationally equivalent (for a sensible
notion of observation), lts.  However, the additions would make the
lts_axiomatic equivalence proof much more difficult.  We also conjecture that
removing the not_blocked from the read-mem transition, and removing the
requirement that the buffer is empty on a Lock label, would give a more liberal,
but equivalent, lts.  Again the lts_axiomatic equivalent proof would be more
difficult.  Should either of these variant machines become useful, we anticipate
being able to prove them equivalent by working solely on the machines.
*)

val _ = Hol_reln `

(!s a v p.
  clause_name "read-mem" /\
  not_blocked s p /\
  (s.M a = SOME v) /\
  no_pending (s.B p) a
  ==>
  machine_trans s 
                (Evt p (Access R (Location_mem a) v)) 
                s) /\

(!s a v p.
  clause_name "read-buffer" /\
  not_blocked s p /\
  (?b1 b2. (s.B p = b1 ++ [(a, v)] ++ b2) /\ no_pending b1 a)
  ==>
  machine_trans s 
                (Evt p (Access R (Location_mem a) v)) 
                s) /\

(!s r v p.
  clause_name "read-reg" /\
  (*not_blocked s p /\*)
  (s.R p r = SOME v)
  ==>
  machine_trans s 
                (Evt p (Access R (Location_reg p r) v)) 
                s) /\

(!s a v p s'.
  clause_name "write-buffer" /\
  (*not_blocked s p /\*)
  (s' = <| R := s.R; 
           M := s.M;
           B := (p =+ (a, v)::s.B p) s.B;
           L := s.L |>)
  ==>
  machine_trans s 
                (Evt p (Access W (Location_mem a) v)) 
                s') /\

(!s a v p b s'.
  clause_name "write-mem" /\
  not_blocked s p /\
  (s.B p = b ++ [(a, v)]) /\
  (s' = <| R := s.R; 
           M := (a =+ SOME v) s.M;
           B := (p =+ b) s.B;
           L := s.L |>)
  ==>
  machine_trans s Tau s') /\

(!s r v p s'.
  clause_name "write-reg" /\
  (*not_blocked s p*)
  (s' = <| R := (p =+ (r =+ SOME v) (s.R p)) s.R;
           M := s.M;
           B := s.B;
           L := s.L |>)
  ==>
  machine_trans s 
                (Evt p (Access W (Location_reg p r) v)) 
                s') /\

(!s p.
  clause_name "barrier" /\
  (*not_blocked s p /\*)
  (s.B p = [])
  ==>
  machine_trans s (Evt p (Barrier Mfence)) s) /\

(!s p b.
  clause_name "nop" /\
  (*not_blocked s p /\*)
  b <> Mfence
  ==>
  machine_trans s (Evt p (Barrier b)) s) /\

(!s p s'.
  clause_name "lock" /\
  (s.L = NONE) /\
  (s.B p = []) /\
  (s' = <| R := s.R;
           M := s.M;
           B := s.B;
           L := SOME p |>)
  ==>
  machine_trans s (Lock p) s') /\

(!s p s'.
  clause_name "unlock" /\
  (s.L = SOME p) /\
  (s.B p = []) /\
  (s' = <| R := s.R;
           M := s.M;
           B := s.B;
           L := NONE |>)
  ==>
  machine_trans s (Unlock p) s')`;

val machine_state_to_state_constraint_def = Define `
  machine_state_to_state_constraint s =
    \l. 
      case l of 
         Location_mem a -> s.M a 
      || Location_reg p r -> s.R p r`;

val machine_final_state_def = Define `
  machine_final_state path =
    if finite path then
      SOME (machine_state_to_state_constraint (last path))
    else
      NONE`; 

val machine_init_state_def = Define `
  machine_init_state sc = 
    <| R := (\p r. sc (Location_reg p r));
       M := (\a. sc (Location_mem a));
       B := (\p. []);
       L := NONE |>`;

val is_init_def = Define `
  is_init s = ?sc. s = machine_init_state sc`;

(* The evt_machine is an annotated version of the above machine to help with the
* lts_axiomatic equivalence proof *)
  
val _ = Hol_datatype `
  evt_machine_state = <|
    (* Per processor registers, annotated with the event that last wrote it *)
    eR : proc -> 'reg -> (value # 'reg event option) option;
    (* main memory, annotated with the event that last wrote it *)
    eM : address -> (value # 'reg event option) option;
    (* Per processor FIFO write buffers *)
    eB : proc -> 'reg event list;
    (* Which processor holds the lock *)
    eL : proc option
  |>`; 

val evt_not_blocked_def = Define `
  evt_not_blocked s p = (s.eL = NONE) \/ (s.eL = SOME p)`;

val evt_no_pending_def = Define `
  evt_no_pending b a = ~(?e. MEM e b /\ (loc e = SOME (Location_mem a)))`;

val _ = Hol_datatype `
  evt_machine_label = 
    TauEvt of 'reg event
  | REvt of 'reg event => 'reg event option
  | WEvt of 'reg event
  | BEvt of 'reg event
  | LockE of proc => 'reg event set
  | UnlockE of proc => 'reg event set`;

val evt_machine_label_11 = fetch "-" "evt_machine_label_11";
val evt_machine_label_distinct = fetch "-" "evt_machine_label_distinct";

val (evt_machine_trans_rules, evt_machine_trans_ind, evt_machine_trans_cases) = Hol_reln `

(!s a v p er ew_opt.
  clause_name "evt-read-mem" /\
  evt_not_blocked s p /\
  (proc er = p) /\
  (er.action = Access R (Location_mem a) v) /\
  (s.eM a = SOME (v, ew_opt)) /\
  evt_no_pending (s.eB p) a
  ==>
  evt_machine_trans s (REvt er ew_opt) s) /\

(!s a v p er ew.
  clause_name "evt-read-buffer" /\
  evt_not_blocked s p /\
  (proc er = p) /\
  (er.action = Access R (Location_mem a) v) /\
  (ew.action = Access W (Location_mem a) v) /\
  (?b1 b2. (s.eB p = b1 ++ [ew] ++ b2) /\ evt_no_pending b1 a)
  ==>
  evt_machine_trans s (REvt er (SOME ew)) s) /\

(!s r v p er ew_opt.
  clause_name "evt-read-reg" /\
  (*evt_not_blocked s p /\*)
  (proc er = p) /\
  (er.action = Access R (Location_reg p r) v) /\
  (s.eR p r = SOME (v, ew_opt))
  ==>
  evt_machine_trans s (REvt er ew_opt) s) /\

(!s a v p ew s'.
  clause_name "evt-write-buffer" /\
  (*evt_not_blocked s p /\*)
  (proc ew = p) /\
  (ew.action = Access W (Location_mem a) v) /\
  (s' = <| eR := s.eR;
           eM := s.eM;
           eB := (p =+ ew::s.eB p) s.eB;
           eL := s.eL |>)
  ==>
  evt_machine_trans s (WEvt ew) s') /\

(!s a v p ew b s'.
  clause_name "evt-write-mem" /\
  evt_not_blocked s p /\
  (proc ew = p) /\
  (ew.action = Access W (Location_mem a) v) /\
  (s.eB p = b ++ [ew]) /\
  (s' = <| eR := s.eR; 
           eM := (a =+ SOME (v, SOME ew)) s.eM;
           eB := (p =+ b) s.eB;
           eL := s.eL |>)
  ==>
  evt_machine_trans s (TauEvt ew) s') /\

(!s r v p ew s'.
  clause_name "evt-write-reg" /\
  (*evt_not_blocked s p /\*)
  (proc ew = p) /\
  (ew.action = Access W (Location_reg p r) v) /\
  (s' = <| eR := (p =+ (r =+ SOME (v, SOME ew)) (s.eR p)) s.eR;
           eM := s.eM;
           eB := s.eB;
           eL := s.eL |>)
  ==>
  evt_machine_trans s (WEvt ew) s') /\

(!s p eb.
  clause_name "evt-barrier" /\
  (*evt_not_blocked s p /\*)
  (proc eb = p) /\
  (eb.action = Barrier Mfence) /\
  (s.eB p = [])
  ==>
  evt_machine_trans s (BEvt eb) s) /\

(!s eb.
  clause_name "evt-nop" /\
  (*not_blocked s p /\*)
  ((eb.action = Barrier Sfence) \/ (eb.action = Barrier Lfence))
  ==>
  evt_machine_trans s (BEvt eb) s) /\

(!s p s' es.
  clause_name "evt-lock" /\
  (s.eL = NONE) /\
  (s.eB p = []) /\
  (s' = <| eR := s.eR;
           eM := s.eM;
           eB := s.eB;
           eL := SOME p |>)
  ==>
  evt_machine_trans s (LockE p es) s') /\

(!s p s' es.
  clause_name "evt-unlock" /\
  (s.eL = SOME p) /\
  (s.eB p = []) /\
  (s' = <| eR := s.eR;
           eM := s.eM;
           eB := s.eB;
           eL := NONE |>)
  ==>
  evt_machine_trans s (UnlockE p es) s')`;

val evt_machine_state_to_state_constraint_def = Define `
  evt_machine_state_to_state_constraint s =
    \l. 
      case l of 
         Location_mem a -> OPTION_MAP FST (s.eM a) 
      || Location_reg p r -> OPTION_MAP FST (s.eR p r)`;

val evt_machine_final_state_def = Define `
  evt_machine_final_state path =
    if finite path then
      SOME (evt_machine_state_to_state_constraint (last path))
    else
      NONE`; 

val evt_machine_init_state_def = Define `
  evt_machine_init_state sc = 
    <| eR := (\p r. OPTION_MAP (\v. (v, NONE)) (sc (Location_reg p r)));
       eM := (\a. OPTION_MAP (\v. (v, NONE)) (sc (Location_mem a)));
       eB := (\p. []);
       eL := NONE |>`;

val evt_is_init_def = Define `
  evt_is_init s = ?sc. s = evt_machine_init_state sc`;

val get_orig_event_def = Define `
  (get_orig_event (REvt e _) = SOME e) /\
  (get_orig_event (WEvt e) = SOME e) /\
  (get_orig_event (BEvt e) = SOME e) /\
  (get_orig_event _ = NONE)`;

val locked_segment_def = Define `
  locked_segment path i j p =
    j + 1 IN PL path /\
    i < j /\
    (?es. nth_label i path = LockE p es) /\
    (?es. nth_label j path = UnlockE p es) /\
    (!k es. i < k /\ k < j ==> nth_label k path <> UnlockE p es)`;

val okEpath_def = Define `
  okEpath E path =
    (* The REvt, WEvt and BEvt labels are exactly the set of events *)
    (E.events = { e | ?i. i + 1 IN PL path /\ (get_orig_event (nth_label i path) = SOME e) }) /\
    (* No REvt, WEvt, or BEvt appears twice as a label *)
    (!i j e1 e2. 
       i + 1 IN PL path /\ j + 1 IN PL path /\ 
       (get_orig_event (nth_label i path) = SOME e1) /\ (get_orig_event (nth_label j path) = SOME e2) /\
       (e1 = e2)
       ==>
       (i = j)) /\
    (* The REvt, WEvt, and BEvt parts of the trace follow po_iico *)
    (!(e1, e2) :: (po_iico E). ?i j. 
       i < j /\ j + 1 IN PL path /\ 
       (get_orig_event (nth_label i path) = SOME e1) /\ (get_orig_event (nth_label j path) = SOME e2)) /\
    (* atomic sets of events are properly bracketed by lock/unlock pairs *)
    (!es :: (E.atomicity). 
       ?i j p. 
         locked_segment path i j p /\
         ({ e | e IN es /\ e IN mem_accesses E }
          = 
          { e | ?k. i < k /\ k < j /\ 
                    (get_orig_event (nth_label k path) = SOME e) /\ 
                    e IN mem_accesses E /\
                    (proc e = p) }))`;

val okMpath_def = Define `
  okMpath path = 
    evt_is_init (first path) /\
    okpath evt_machine_trans path /\
    !i e. 
      i + 1 IN PL path /\ (nth_label i path = WEvt e) /\ is_mem_access e
      ==>
      ?j. j + 1 IN PL path /\ i < j /\ (nth_label j path = TauEvt e)`;

(* Relates s in the event annotated machine to s' in the unannotated machine
* iff s erases the annotations to become s' *)
val erase_state_def = Define `
  erase_state s s' =
    (!p r. s'.R p r = OPTION_MAP FST (s.eR p r)) /\
    (!a. s'.M a = OPTION_MAP FST (s.eM a)) /\
    (!p. (LENGTH (s'.B p) = LENGTH (s.eB p)) /\ 
       !n. n < LENGTH (s.eB p) ==> 
         ?e a v. (EL n (s.eB p) = e) /\
                 (proc e = p) /\ 
                 (e.action = Access W (Location_mem a) v) /\
                 (EL n (s'.B p) = (a, v))) /\
    (s'.L = s.eL)`;

val erase_label_def = Define `
  (erase_label (TauEvt _) = Tau) /\
  (erase_label (REvt e _) = Evt (proc e) e.action) /\
  (erase_label (WEvt e) = Evt (proc e) e.action) /\
  (erase_label (BEvt e) = Evt (proc e) e.action) /\
  (erase_label (LockE p es) = Lock p) /\
  (erase_label (UnlockE p es) = Unlock p)`;

val annotated_labels_def = Define `
(annotated_labels Tau ew e_opt = { TauEvt ew }) /\
(annotated_labels (Evt p (Access R l v)) ew e_opt =
       { REvt e e_opt | e | (e.action = Access R l v) /\ (p = proc e) }) /\
(annotated_labels (Evt p (Access W l v)) ew e_opt =
       { WEvt e | (e.action = Access W l v) /\ (p = proc e) }) /\
(annotated_labels (Evt p (Barrier b)) ew e_opt =
       { BEvt e | (e.action = Barrier b) /\ (p = proc e) }) /\
(annotated_labels (Lock p) ew e_opt =
       { LockE p es | es | T }) /\
(annotated_labels (Unlock p) ew e_opt =
       { UnlockE p es | es | T })`;

val _ = export_theory ();