Require Import Vbase.
Set Implicit Arguments.
Definition actid := nat.
Inductive act :=
| Askip
| Aload (l : nat) (v : nat)
| Astore (l : nat) (v : nat)
| Armw (l : nat) (v v': nat).
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.
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.
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.
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