(*        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 "moretypesettingScript.sml";
app load ["lts_memory_modelTheory", "HolDoc", "Net_Hol_reln",
          "axiomatic_memory_modelTheory","typesettingTheory"];
*)


open HolKernel boolLib Parse bossLib;

open lts_memory_modelTheory typesettingTheory axiomatic_memory_modelTheory;

open HolDoc Net_Hol_reln;


val _ = new_theory "moretypesetting";

(* MACHINE TYPESETTING *)


(* -------------------------------------------------- *)
(*                Rule prep                           *)
(* -------------------------------------------------- *)

val _ = add_rule { block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)),
                   paren_style = OnlyIfNecessary,
                   fixity = Infix(NONASSOC, 420),
                   pp_elements = [HardSpace 1, TOK "/*", HardSpace 1,
                                  TM (* proto *), TOK ",", HardSpace 1,
                                  TM (* cat *), HardSpace 1,
                                  TOK "*/", BreakSpace(1,0),
                                  TM, (* host0 *)
                                  BreakSpace(1,2), TOK "--", HardSpace 1,
                                  TM, (* label *)
                                  HardSpace 1, TOK "-->", BreakSpace(1,0)],
                   term_name = "host_redn0"
                   };

val _ = add_rule { block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)),
                   paren_style = OnlyIfNecessary,
                   fixity = Infix(NONASSOC, 420),
                   pp_elements = [HardSpace 1, TOK "/*", HardSpace 1,
                                  TM (* proto *), TOK ",", HardSpace 1,
                                  TM (* cat *), HardSpace 1,
                                  TOK "*/", BreakSpace(1,0),
                                  TM, (* host0 *)
                                  BreakSpace(1,2), TOK "--", HardSpace 1,
                                  TM, (* label *)
                                  HardSpace 1, TOK "--=>", BreakSpace(1,0)],
                   term_name = "host_redn"
                   };

val _ = add_rule { block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)),
                   paren_style = OnlyIfNecessary,
                   fixity = Infixl 199,
                   pp_elements = [BreakSpace(1,~2), TOK "<==", HardSpace 1],
                   term_name = "revimp" };

val revimp_def = xDefine "revimp" `(q <== p) = (p ==> q)` (*: @norender :*);



val _ = Define `
  UPD f k v = (k=+v)f`;

val (host_redn0_rules, host_redn0_ind, host_redn0_cases) =
  Net_Hol_reln`

   (!s a v p.

   read_mem /* tcp,rc (*: Read from memory :*) */
     s
   -- Evt p (Access R (Location_mem a) v) -->
     s

  <==

     not_blocked s p /\ (s.M a = SOME v) /\  no_pending (s.B p) a 


   ) /\


   (!s a v p.

   read_buffer /* rp_tcp,rc (*: Read from write buffer :*) */
     s
   -- Evt p (Access R (Location_mem a) v) -->
     s

  <==

     not_blocked s p /\  (?b1 b2. (s.B p = b1 ++ [(a, v)] ++ b2) /\ no_pending b1 a)


   ) /\


   (!s r v p.

   read_reg /* rp_tcp,rc (*: Read from register :*) */
     s
   -- Evt p (Access R (Location_reg p r) v)  -->
     s

  <==

     (s.R p r = SOME v)


   ) /\


   (!s a v p.

   write_buffer /* rp_tcp,rc (*: Write to write buffer :*) */
     s
   -- Evt p (Access W (Location_mem a) v)  -->
     s with <| B := UPD s.B p ([(a, v)] ++ (s.B p))|>

  <==

     (*not_blocked s p /\*) T


   ) /\


   (!s a v p b.

   write_mem /* rp_tcp,rc (*: Write from write buffer to memory:*) */
     s
   -- Tau  -->
     s with <| M := UPD s.M a  (SOME v); B := UPD s.B p b |>

  <==

   not_blocked s p /\ (s.B p = b ++ [(a, v)]) 


   ) /\


   (!s r v p.

   write_reg /* rp_tcp,rc (*: Write to register :*) */
     s
   -- Evt p (Access W (Location_reg p r) v) -->
     s with <| R := UPD s.R p ((UPD ((s.R p)) r (SOME v))) |>

  <==

    T


   ) /\


   (!s p b.

   barrier /* rp_tcp,rc (*: Barrier :*) */
     s
   -- Evt p (Barrier b)  -->
     s

  <==

  (*not_blocked s p /\*)(b = Mfence) ==> (s.B p = [])


   ) /\


   (!s p.

   lock /* rp_tcp,rc (*: Lock :*) */
     s
   -- Lock p  -->
     s with <| L := SOME p |>

  <==

  (s.L = NONE) /\ (s.B p = []) 


   ) /\


   (!s p.

   unlock /* rp_tcp,rc (*: Unlock :*) */
     s
   -- Unlock p -->
     s with <| L := NONE |>

  <==

  (s.L = SOME p) /\ (s.B p = []) 


   )`;

(* END OF EXPERIMENT *)

val _ = export_theory ();