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.
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.
Fence instructions.
Non-atomic actions have memory order na.
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.
Lemma is_acquire_readE a :
is_acquire_read a ↔ is_acquire a ∧ is_read a.
Lemma is_acquire_fenceE a :
is_acquire_fence a ↔ is_acquire a ∧ is_fence a.
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.
Lemma is_release_writeE a :
is_release_write a ↔ is_release a ∧ is_write a.
Lemma is_release_fenceE a :
is_release_fence a ↔ is_release a ∧ is_fence a.
Lemma is_readLV_rmw_writeL a l v : is_readLV a l v → is_rmw a → is_writeL a l.
Lemma is_readL_rmw_writeL a l : is_readL a l → is_rmw a → is_writeL a l.
Lemma is_writeLV_writeL a l v : is_writeLV a l v → is_writeL a l.
Lemmas deriving is_readL.
Lemma is_writeLV_rmw_readL a l v : is_writeLV a l v → is_rmw a → is_readL a l.
Lemma is_writeL_rmw_readL a l : is_writeL a l → is_rmw a → is_readL a l.
Lemma is_readLV_readL a l v : is_readLV a l v → is_readL a l.
Lemmas deriving is_accessL.
Lemma is_writeL_accessL a l : is_writeL a l → is_accessL a l.
Lemma is_readL_accessL a l : is_readL a l → is_accessL a l.
Lemma is_writeLV_accessL a l v : is_writeLV a l v → is_accessL a l.
Lemma is_readLV_accessL a l v : is_readLV a l v → is_accessL a l.
Lemmas deriving is_write.
Lemma is_rmw_write :
∀ a, is_rmw a → is_write a.
Lemma is_writeLV_write :
∀ a l v, is_writeLV a l v → is_write a.
Lemma is_writeL_write :
∀ a l, is_writeL a l → is_write a.
Lemma is_release_write_write :
∀ a, is_release_write a → is_write a.
Lemmas deriving is_read.
Lemma is_rmw_read :
∀ a, is_rmw a → is_read a.
Lemma is_readLV_read :
∀ a l v, is_readLV a l v → is_read a.
Lemma is_readL_read :
∀ a l, is_readL a l → is_read a.
Lemma is_acquire_read_read :
∀ a, is_acquire_read a → is_read a.
Lemmas deriving is_access.
Lemma is_accessL_access a l : is_accessL a l → is_access a.
Lemma is_write_access a : is_write a → is_access a.
Lemma is_writeL_access a l : is_writeL a l → is_access a.
Lemma is_writeLV_access a l v : is_writeLV a l v → is_access a.
Lemma is_read_access a : is_read a → is_access a.
Lemma is_readL_access a l : is_readL a l → is_access a.
Lemma is_readLV_access a l v : is_readLV a l v → is_access a.
Lemma is_rmw_access a : is_rmw a → is_access a.
Lemma is_na_access a : is_na a → is_access a.
Lemma is_release_write_access:
∀ a, is_release_write a → is_access a.
Lemma is_acquire_read_access:
∀ a, is_acquire_read a → is_access a.
Lemmas deriving is_fence.
Lemma is_release_fence_fence:
∀ a, is_release_fence a → is_fence a.
Lemma is_acquire_fence_fence:
∀ a, is_acquire_fence a → is_fence a.
Lemmas deriving is_acquire.
Lemma is_acquire_read_acquire :
∀ a, is_acquire_read a → is_acquire a.
Lemma is_acquire_fence_acquire :
∀ a, is_acquire_fence a → is_acquire a.
Lemmas deriving is_release.
Lemma is_release_write_release :
∀ a, is_release_write a → is_release a.
Lemma is_release_fence_release :
∀ a, is_release_fence a → is_release a.
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