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.

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.

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 _ FATsctrue
    | _false
  end.

Acquire actions have memory order acq or stronger.

Definition is_acquire_rtyp t :=
   match t with RATsc | RATacqtrue | _false end.

Definition is_acquire_utyp t :=
   match t with UATsc | UATacq | UATrel_acqtrue | _false end.

Definition is_acquire_ftyp t :=
   match t with FATsc | FATacq | FATrel_acqtrue | _false end.

Definition is_acquire a :=
  match a with
    | Aload _ typ _ _is_acquire_rtyp typ
    | Armw _ typ _ _ _is_acquire_utyp typ
    | Afence _ typis_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 _ typis_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 | WATreltrue | _false end.

Definition is_release_utyp t :=
   match t with UATsc | UATrel | UATrel_acqtrue | _false end.

Definition is_release_ftyp t :=
   match t with FATsc | FATrel | FATrel_acqtrue | _false end.

Definition is_release a :=
  match a with
    | Astore _ typ _ _is_release_wtyp typ
    | Armw _ typ _ _ _is_release_utyp typ
    | Afence _ typis_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 _ typis_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.

Lemmas about access types

Lemmas deriving is_writeL.
Lemmas deriving is_readL.

Lemma is_writeLV_rmw_readL a l v : is_writeLV a l vis_rmw ais_readL a l.

Lemma is_writeL_rmw_readL a l : is_writeL a lis_rmw ais_readL a l.

Lemma is_readLV_readL a l v : is_readLV a l vis_readL a l.

Lemmas deriving is_accessL.
Lemmas deriving is_write.

Lemma is_rmw_write :
   a, is_rmw ais_write a.

Lemma is_writeLV_write :
   a l v, is_writeLV a l vis_write a.

Lemma is_writeL_write :
   a l, is_writeL a lis_write a.

Lemma is_release_write_write :
   a, is_release_write ais_write a.

Lemmas deriving is_read.

Lemma is_rmw_read :
   a, is_rmw ais_read a.

Lemma is_readLV_read :
   a l v, is_readLV a l vis_read a.

Lemma is_readL_read :
   a l, is_readL a lis_read a.

Lemma is_acquire_read_read :
   a, is_acquire_read ais_read a.

Lemmas deriving is_access.
Lemmas deriving is_fence.
Lemmas deriving is_acquire.
Lemmas deriving is_release.

This page has been generated by coqdoc