Definition of C11 actions


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).

The function thread a returns the thread identifier of action a.

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.

Definition is_fence a :=
  match a with
    | Afence _ _ => true
    | _ => false
  end.

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.

Lemmas about access types

Lemmas deriving is_writeL.

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.

This page has been generated by coqdoc