Require Import Vbase.
Set Implicit Arguments.
Definition actid := nat.
Definition thread_id := nat.
Inductive read_access_type :=
| RATacq.
Inductive write_access_type :=
| WATrel.
Inductive rmw_access_type :=
| UATrel_acq.
Inductive act :=
| Askip (tid: thread_id)
| 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).
Definition thread a :=
match a with
| Askip 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 _ ⇒ 0
| Aload _ _ l _
| Astore _ _ l _
| Armw _ _ l _ _ ⇒ l
end.
Definition is_access a :=
match a with
| Aload _ _ _ _ | Astore _ _ _ _ | Armw _ _ _ _ _ ⇒ true
| Askip _ ⇒ false
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.
Definition is_read_only a :=
match a with
| Askip _ ⇒ false
| Aload _ _ _ _ ⇒ true
| Armw _ _ _ _ _ ⇒ false
| Astore _ _ _ _ ⇒ 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.
Definition is_write_only a :=
match a with
| Askip _ ⇒ false
| Aload _ _ _ _ ⇒ false
| Armw _ _ _ _ _ ⇒ false
| Astore _ _ _ _ ⇒ true
end.
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.
Acquire actions have memory order acq or stronger.
Definition is_acquire_rtyp t :=
match t with RATacq ⇒ true end.
Definition is_acquire_utyp t :=
match t with UATrel_acq ⇒ true end.
Definition is_acquire a :=
match a with
| Aload _ typ _ _ ⇒ is_acquire_rtyp typ
| Armw _ typ _ _ _ ⇒ is_acquire_utyp typ
| _ ⇒ false
end.
Release actions have memory order rel or stronger.
Definition is_release_wtyp t :=
match t with WATrel ⇒ true end.
Definition is_release_utyp t :=
match t with | UATrel_acq ⇒ true end.
Definition is_release_write a :=
match a with
| Astore _ typ _ _ ⇒ is_release_wtyp typ
| Armw _ typ _ _ _ ⇒ is_release_utyp typ
| _ ⇒ false
end.
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_write.
Lemma is_rmw_write :
∀ a, is_rmw a → is_write a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_writeLV_write :
∀ a l v, is_writeLV a l v → is_write a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_writeL_write :
∀ a l, is_writeL a l → is_write a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_release_write_write :
∀ a, is_release_write a → is_write a.
Proof. by destruct a; ins; desf. Qed.
Lemmas deriving is_read.
Lemma is_rmw_read :
∀ a, is_rmw a → is_read a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_readLV_read :
∀ a l v, is_readLV a l v → is_read a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_readL_read :
∀ a l, is_readL a l → is_read a.
Proof. by destruct a; ins; desf. Qed.
Lemma is_readL_loc : ∀ x l, is_readL x l →
loc x = l.
Proof. by destruct x; ins; desf. Qed.
Lemma is_writeL_loc : ∀ x l, is_writeL x l →
loc x = l.
Proof. by destruct x; ins; desf. Qed.
Lemma is_readLV_loc : ∀ x l v, is_readLV x l v →
loc x = l.
Proof. by destruct x; ins; desf. Qed.
Lemma is_writeLV_loc : ∀ x l v, is_writeLV x l v →
loc x = l.
Proof. by destruct x; ins; desf. Qed.
Lemma is_write_write_only : ∀ x, is_write_only x = true →
is_write x = true.
Proof.
ins; destruct x; simpl in *; auto.
Qed.
Lemma is_read_read_only : ∀ x, is_read_only x = true →
is_read x = true.
Proof.
ins; destruct x; simpl in *; auto.
Qed.
Hint Resolve
is_writeLV_writeL is_readLV_readL
is_writeL_write is_writeLV_write is_rmw_write
is_readL_read is_readLV_read is_rmw_read
is_readL_loc is_writeL_loc
is_readLV_loc is_writeLV_loc : caccess.
Lemma is_write_access a : is_write a → is_access a.
Proof. by destruct a. Qed.
Lemma is_read_access a : is_read 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_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. Qed.
Hint Resolve is_read_access is_readL_access is_readLV_access
is_write_access is_writeL_access : caccess.
Lemma is_read_only_access a : is_read_only a → is_access a.
Proof. by destruct a. Qed.
Lemma is_write_only_access a : is_write_only a → is_access a.
Proof. by destruct a. Qed.
Lemma is_read_only_read a : is_read_only a → is_read a.
Proof. by destruct a. Qed.
Lemma is_write_only_write a : is_write_only a → is_write a.
Proof. by destruct a. Qed.
Hint Resolve is_read_only_read is_read_only_access
is_write_only_write is_write_only_access : caccess.
This page has been generated by coqdoc