Require Import Vbase.
Set Implicit Arguments.
Definition actid := nat.
Definition thread_id := nat.
Inductive read_access_type :=
| RATsc
| RATacq
| RATrlx
| RATna.
Inductive write_access_type :=
| WATsc
| WATrel
| WATrlx
| WATna.
Inductive rmw_access_type :=
| UATsc
| UATrel_acq
| UATacq
| UATrel
| UATrlx .
Inductive fence_access_type :=
| FATacq
| FATrel
| FATrel_acq
| FATsc.
Inductive act :=
| Askip (tid: thread_id)
| Aalloc (tid: thread_id) (l n : nat)
| Aload (tid: thread_id) (typ : read_access_type) (l : nat) (v : nat)
| Astore (tid: thread_id) (typ : write_access_type) (l : nat) (v : nat)
| Armw (tid: thread_id) (typ : rmw_access_type) (l : nat) (v v': nat)
| Afence (tid: thread_id) (typ : fence_access_type).
Definition thread a :=
match a with
| Askip tid
| Afence tid _
| Aalloc tid _ _
| Aload tid _ _ _
| Astore tid _ _ _
| Armw tid _ _ _ _ => tid
end.
The function loc a returns the location accessed by action a. If a
is not an access, it returns a bogus location.
Definition loc a :=
match a with
| Askip _
| Afence _ _ => 0
| Aalloc _ l _
| Aload _ _ l _
| Astore _ _ l _
| Armw _ _ l _ _ => l
end.
A read is either a load or a read-modify-write action.
Definition is_read a :=
match a with
| Aload _ _ _ _ | Armw _ _ _ _ _ => true
| _ => false
end.
Definition is_readL a l :=
match a with
| Aload _ _ l' _
| Armw _ _ l' _ _ => l' = l
| _ => False
end.
Definition is_readLV a l v :=
match a with
| Aload _ _ l' v'
| Armw _ _ l' v' _ => l' = l /\ v' = v
| _ => False
end.
A write is either a store or a read-modify-write action.
Definition is_write a :=
match a with
| Astore _ _ _ _ | Armw _ _ _ _ _ => true
| _ => false
end.
Definition is_writeL a l :=
match a with
| Astore _ _ l' _
| Armw _ _ l' _ _ => l' = l
| _ => False
end.
Definition is_writeLV a l v :=
match a with
| Astore _ _ l' v'
| Armw _ _ l' _ v' => l' = l /\ v' = v
| _ => False
end.
A read-modify-write action is both a read and a write
Definition is_rmw a :=
match a with
| Armw _ _ _ _ _ => true
| _ => false
end.
Lemma is_rmwE a : is_rmw a <-> is_read a /\ is_write a.
Proof. destruct a; ins; intuition. Qed.
A memory access is either a read or a write.
Definition is_access a :=
match a with
| Aload _ _ _ _ | Astore _ _ _ _ | Armw _ _ _ _ _ => true
| _ => false
end.
Definition is_accessL a l :=
match a with
| Aload _ _ l' _ | Astore _ _ l' _ | Armw _ _ l' _ _ => l' = l
| _ => False
end.
Lemma is_accessE a : is_access a <-> is_read a \/ is_write a.
Proof. destruct a; ins; intuition. Qed.
Fence instructions.
Non-atomic actions have memory order na.
Definition is_na a :=
match a with
| Aload _ RATna _ _
| Astore _ WATna _ _ => true
| _ => false
end.
Sequentially consistent actions have memory order sc.
Definition is_sc a :=
match a with
| Aload _ RATsc _ _
| Astore _ WATsc _ _
| Armw _ UATsc _ _ _
| Afence _ FATsc => true
| _ => false
end.
Acquire actions have memory order acq or stronger.
Definition is_acquire_rtyp t :=
match t with RATsc | RATacq => true | _ => false end.
Definition is_acquire_utyp t :=
match t with UATsc | UATacq | UATrel_acq => true | _ => false end.
Definition is_acquire_ftyp t :=
match t with FATsc | FATacq | FATrel_acq => true | _ => false end.
Definition is_acquire a :=
match a with
| Aload _ typ _ _ => is_acquire_rtyp typ
| Armw _ typ _ _ _ => is_acquire_utyp typ
| Afence _ typ => is_acquire_ftyp typ
| _ => false
end.
Definition is_acquire_read a :=
match a with
| Aload _ typ _ _ => is_acquire_rtyp typ
| Armw _ typ _ _ _ => is_acquire_utyp typ
| _ => false
end.
Definition is_acquire_fence a :=
match a with
| Afence _ typ => is_acquire_ftyp typ
| _ => false
end.
Lemma is_acquireE a :
is_acquire a <-> is_acquire_read a \/ is_acquire_fence a.
Proof. by destruct a; ins; intuition. Qed.
Lemma is_acquire_readE a :
is_acquire_read a <-> is_acquire a /\ is_read a.
Proof. by destruct a; ins; intuition. Qed.
Lemma is_acquire_fenceE a :
is_acquire_fence a <-> is_acquire a /\ is_fence a.
Proof. by destruct a; ins; intuition. Qed.
Release actions have memory order rel or stronger.
Definition is_release_wtyp t :=
match t with WATsc | WATrel => true | _ => false end.
Definition is_release_utyp t :=
match t with UATsc | UATrel | UATrel_acq => true | _ => false end.
Definition is_release_ftyp t :=
match t with FATsc | FATrel | FATrel_acq => true | _ => false end.
Definition is_release a :=
match a with
| Astore _ typ _ _ => is_release_wtyp typ
| Armw _ typ _ _ _ => is_release_utyp typ
| Afence _ typ => is_release_ftyp typ
| _ => false
end.
Definition is_release_write a :=
match a with
| Astore _ typ _ _ => is_release_wtyp typ
| Armw _ typ _ _ _ => is_release_utyp typ
| _ => false
end.
Definition is_release_fence a :=
match a with
| Afence _ typ => is_release_ftyp typ
| _ => false
end.
Lemma is_releaseE a :
is_release a <-> is_release_write a \/ is_release_fence a.
Proof. by destruct a; ins; intuition. Qed.
Lemma is_release_writeE a :
is_release_write a <-> is_release a /\ is_write a.
Proof. by destruct a; ins; intuition. Qed.
Lemma is_release_fenceE a :
is_release_fence a <-> is_release a /\ is_fence a.
Proof. by destruct a; ins; intuition. Qed.
Lemma is_readLV_rmw_writeL a l v : is_readLV a l v -> is_rmw a -> is_writeL a l.
Proof. by destruct a; ins; desf. Qed.
Lemma is_readL_rmw_writeL a l : is_readL a l -> is_rmw a -> is_writeL a l.
Proof. by destruct a; ins; desf. Qed.
Lemma is_writeLV_writeL a l v : is_writeLV a l v -> is_writeL a l.
Proof. by destruct a; ins; desf. Qed.
Lemmas deriving is_readL.
Lemma is_writeLV_rmw_readL a l v : is_writeLV a l v -> is_rmw a -> is_readL a l.
Proof. by destruct a; ins; desf. Qed.
Lemma is_writeL_rmw_readL a l : is_writeL a l -> is_rmw a -> is_readL a l.
Proof. by destruct a; ins; desf. Qed.
Lemma is_readLV_readL a l v : is_readLV a l v -> is_readL a l.
Proof. by destruct a; ins; desf. Qed.
Lemmas deriving is_accessL.
Lemma is_writeL_accessL a l : is_writeL a l -> is_accessL a l.
Proof. by destruct a. Qed.
Lemma is_readL_accessL a l : is_readL a l -> is_accessL a l.
Proof. by destruct a. Qed.
Lemma is_writeLV_accessL a l v : is_writeLV a l v -> is_accessL a l.
Proof. by destruct a; ins; desf. Qed.
Lemma is_readLV_accessL a l v : is_readLV a l v -> is_accessL a l.
Proof. by destruct a; ins; desf. Qed.
Lemmas deriving is_write.
Lemma is_rmw_write :
forall a, is_rmw a -> is_write a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_writeLV_write :
forall a l v, is_writeLV a l v -> is_write a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_writeL_write :
forall a l, is_writeL a l -> is_write a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_release_write_write :
forall a, is_release_write a -> is_write a.
Proof. by destruct a; ins; desf. Qed.
Lemmas deriving is_read.
Lemma is_rmw_read :
forall a, is_rmw a -> is_read a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_readLV_read :
forall a l v, is_readLV a l v -> is_read a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_readL_read :
forall a l, is_readL a l -> is_read a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_acquire_read_read :
forall a, is_acquire_read a -> is_read a.
Proof. by destruct a; ins; desf. Qed.
Lemmas deriving is_access.
Lemma is_accessL_access a l : is_accessL a l -> is_access a.
Proof. by destruct a. Qed.
Lemma is_write_access a : is_write a -> is_access a.
Proof. by destruct a. Qed.
Lemma is_writeL_access a l : is_writeL a l -> is_access a.
Proof. by destruct a. Qed.
Lemma is_writeLV_access a l v : is_writeLV a l v -> is_access a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_read_access a : is_read a -> is_access a.
Proof. by destruct a. Qed.
Lemma is_readL_access a l : is_readL a l -> is_access a.
Proof. by destruct a. Qed.
Lemma is_readLV_access a l v : is_readLV a l v -> is_access a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_rmw_access a : is_rmw a -> is_access a.
Proof. by destruct a. Qed.
Lemma is_na_access a : is_na a -> is_access a.
Proof. by destruct a. Qed.
Lemma is_release_write_access:
forall a, is_release_write a -> is_access a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_acquire_read_access:
forall a, is_acquire_read a -> is_access a.
Proof. by destruct a; ins; desf. Qed.
Lemmas deriving is_fence.
Lemma is_release_fence_fence:
forall a, is_release_fence a -> is_fence a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_acquire_fence_fence:
forall a, is_acquire_fence a -> is_fence a.
Proof. by destruct a; ins; desf. Qed.
Lemmas deriving is_acquire.
Lemma is_acquire_read_acquire :
forall a, is_acquire_read a -> is_acquire a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_acquire_fence_acquire :
forall a, is_acquire_fence a -> is_acquire a.
Proof. by destruct a; ins; desf. Qed.
Lemmas deriving is_release.
Lemma is_release_write_release :
forall a, is_release_write a -> is_release a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_release_fence_release :
forall a, is_release_fence a -> is_release a.
Proof. by destruct a; ins; desf. Qed.
Hint Immediate
is_readLV_rmw_writeL is_readL_rmw_writeL is_writeLV_writeL
is_writeLV_rmw_readL is_writeL_rmw_readL is_readLV_readL
is_writeL_accessL is_writeLV_accessL
is_writeL_write is_writeLV_write is_rmw_write is_release_write_write
is_readL_read is_readLV_read is_rmw_read is_acquire_read_read
is_read_access is_readL_accessL is_readLV_accessL
is_write_access is_writeL_access is_writeLV_access
is_readL_access is_readLV_access
is_accessL_access is_rmw_access is_na_access
is_release_write_access is_acquire_read_access
is_release_fence_fence is_acquire_fence_fence
is_release_write_release is_acquire_read_acquire
is_release_fence_release is_acquire_fence_acquire : access.
This page has been generated by coqdoc