Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple fsltriple2.
Require Import ihc initread.
Require Import GpsSepAlg.

Set Implicit Arguments.

A helper lemma for establishing the soundness of the atomic load rules.

Definition preciseish PS PSg P :=
   hP (SEM: assn_sem P hP) hP' (SEM': assn_sem P hP')
         hF (DEF: hplus hP hF @Hundef PS PSg) hF' (EQ: hplus hP hF = hplus hP' hF'),
  hP = hP' Hsim hF hF'.

Lemma precise_nabla PS PSg (P: assn PS PSg): precise P preciseish (Anabla P).

Atomic loads


Theorem rule_load_acq PS PSg typ E QQ
                     (PREC: v, @precise PS PSg (QQ v))
                     (NORM: v, normalizable (QQ v))
                     (TYP : acquire_typ typ) :
  triple (Astar (Aacq E QQ) (Arainit E))
         (Eload typ E)
         (fun vAstar (Aacq E (hupd QQ v Aemp)) (Astar (Arainit E) (QQ v))).

Theorem rule_load_rlx PS PSg typ E QQ
    (PREC: v, @precise PS PSg (QQ v))
    (NORM: v, normalizable (QQ v))
    (AT: typ ATna):
  triple (Astar (Aacq E QQ) (Arainit E))
         (Eload typ E)
         (fun vAstar (Aacq E (hupd QQ v Aemp)) (Astar (Arainit E) (Anabla (QQ v)))).


This page has been generated by coqdoc