Module InjectedCode

Require Ast Op.
Require Import Coqlib Integers Pointers Maps.

Require Import MIR INJECT RTLinject DataStructures Common.

Some notation to easily write injected code.


Control flow.
Notation "s1 ';;' s2" := (Sseq s1 s2) (at level 81, right associativity, format "'[v' '[' s1 ';;' ']' '//' '[' s2 ']' ']'") : inject_scope.
Notation "'If' r1 '=' r2 'Then' s1 'Else' s2" := (Sifthenelse (Op.Ccomp Ceq) (r1::r2::(@nil positive)) s1 s2) (at level 80, left associativity, r1 at level 50, r2 at level 50) : inject_scope.
Notation "'If' r1 '≠' r2 'Then' s1 'Else' s2" := (Sifthenelse (Op.Ccomp Cne) (r1::r2::(@nil positive)) s1 s2) (at level 80, left associativity, r1 at level 50, r2 at level 50) : inject_scope.
Notation "'If' r1 '==' imm 'Then' s1 'Else' s2" := (Sifthenelse (Op.Ccompimm Ceq imm) (r1::(@nil positive)) s1 s2) (at level 80, left associativity, r1 at level 50) : inject_scope.
Notation "'If' r1 '≥' imm 'Then' s1 'Else' s2" := (Sifthenelse (Op.Ccompimm Cge imm) (r1::(@nil positive)) s1 s2) (at level 80, left associativity, r1 at level 50) : inject_scope.
Notation "'If' r1 '<>' imm 'Then' s1 'Else' s2" := (Sifthenelse (Op.Ccompimm Cne imm) (r1::(@nil positive)) s1 s2) (at level 80, left associativity, r1 at level 50) : inject_scope.
Notation "'While' r1 'Do' body " := (Swhile (Op.Ccompimm Cne Int.zero) (r1::(@nil positive)) body) (at level 80, left associativity, r1 at level 50) : inject_scope.
Notation "'While' r1 '≠' r2 'Do' body " := (Swhile (Op.Ccomp Cne) (r1::r2::(@nil positive)) body) (at level 80, left associativity, r1 at level 50, r2 at level 50) : inject_scope.
Notation "'While' r1 '<>' imm 'Do' body " := (Swhile (Op.Ccompimm Cne imm) (r1::(@nil positive)) body) (at level 80, left associativity, r1 at level 50) : inject_scope.
Notation "'Repeat' body 'Until' r1 '=' r2" := (Srepeat body (Op.Ccomp Ceq) (r1::r2::(@nil positive))) (at level 80, left associativity, r1 at level 50, r2 at level 50) : inject_scope.
Notation "'Repeat' body 'Until' r1 '==' imm" := (Srepeat body (Op.Ccompimm Ceq imm) (r1::(@nil positive))) (at level 80, left associativity, r1 at level 50, r2 at level 50) : inject_scope.
Notation "'Repeat' body 'Until' r1 " := (Srepeat body (Op.Ccompimm Cne Int.zero) (r1::(@nil positive))) (at level 80, left associativity, r1 at level 50) : inject_scope.

Local computation.
Notation "'Lea_g' dst ':=' ident" := (Sop (Op.Olea (Op.Aglobal ident Int.zero)) (@nil positive) dst) (at level 60, ident at level 45) : inject_scope.
Notation "'Lea_g' dst ':=' ident '[' idx ']'" := (Sop (Op.Olea (Op.Abased ident Int.zero)) (idx::(@nil positive)) dst) (at level 60, ident at level 45) : inject_scope.
Notation "'Lea_i' dst ':=' ident '[' idx ']'" := (Sop (Op.Olea (Op.Aglobal ident idx)) (@nil positive) dst) (at level 60) : inject_scope.
Notation "'Lea' dst ':=' src '[' idx ']'" := (Sop (Op.Olea (Op.Aindexed idx)) (src::(@nil positive)) dst) (at level 60, src at level 45, idx at level 45) : inject_scope.
Notation "'Lea' dst ':=' src '+' idx " := (Sop (Op.Olea (Op.Aindexed2 Int.zero)) (src::idx::(@nil positive)) dst) (at level 60, src at level 45, idx at level 45) : inject_scope.
Notation "'Lea_s' dst ':=' imm" := (Sop (Op.Olea (Op.Ainstack imm)) (@nil positive) dst) (at level 60) : inject_scope.
Notation "'Move' dst ':=' src" := (Sop Op.Omove (src::(@nil positive)) dst) (at level 60) : inject_scope.
Notation "'Const' dst ':=' v" := (Sop (Op.Ointconst v) (@nil positive) dst) (at level 60) : inject_scope.
Notation "'Shl' dst ':=' src '<<' imm" := (Sop (Op.Oshlimm imm) (src::(@nil positive)) dst) (at level 60) : inject_scope.
Notation "'Or' dst ':=' src '|' imm" := (Sop (Op.Oorimm imm) (src::(@nil positive)) dst) (at level 60) : inject_scope.
Notation "'Xor' dst ':=' src '^' imm" := (Sop (Op.Oxorimm imm) (src::(@nil positive)) dst) (at level 60, src at level 20) : inject_scope.
Notation "'Cmp' dst ':=' src '==' imm" := (Sop (Op.Ocmp (Op.Ccompimm Ceq imm)) (src::(@nil positive)) dst) (at level 60, src at level 45, imm at level 45) : inject_scope.
Notation "'Cmp' dst ':=' src '<>' imm" := (Sop (Op.Ocmp (Op.Ccompimm Cne imm)) (src::(@nil positive)) dst) (at level 60, src at level 45, imm at level 45) : inject_scope.
Notation "'Cmp' dst ':=' src '=' cmp" := (Sop (Op.Ocmp (Op.Ccomp Ceq)) (src::cmp::(@nil positive)) dst) (at level 60, src at level 45, cmp at level 45) : inject_scope.
Notation "'Cmp' dst ':=' src '≠' cmp" := (Sop (Op.Ocmp (Op.Ccomp Cne)) (src::cmp::(@nil positive)) dst) (at level 60, src at level 45, cmp at level 45) : inject_scope.

Reads and writes.
Notation "'Load' dst ':=' ptr" := (Sload Global (Op.Aindexed Int.zero) (ptr::nil) dst)(at level 60, ptr at level 45) : inject_scope.
Notation "'Load' dst ':=' ptr '[' idx ']'" := (Sload Global (Op.Aindexed idx) (ptr::nil) dst)(at level 60, ptr at level 45) : inject_scope.
Notation "'Load' dst ':=' ptr '+' idx '[' off ']'" := (Sload Global (Op.Aindexed2 off) (ptr::idx::nil) dst)(at level 60, ptr at level 45, idx at level 45) : inject_scope.
Notation "'Load' dst ':=' ptr '+' idx '×' sc '[' off ']'" :=
  (Sload Global (Op.Aindexed2scaled sc off) (ptr::idx::nil) dst)
  (at level 60, ptr at level 45, idx at level 45, sc at level 45, off at level 45) : inject_scope.
Notation "'Load_s' dst ':=' soff " := (Sload Global (Op.Ainstack soff) (@nil positive) dst)(at level 60) : inject_scope.
Notation "'Load_g' dst ':=' ident " := (Sload Global (Op.Aglobal ident Int.zero) (@nil positive) dst)(at level 60, ident at level 45) : inject_scope.
Notation "'Load_g' dst ':=' ident '[' idx ']'" := (Sload Global (Op.Abased ident Int.zero) (idx::(@nil positive)) dst)(at level 60, ident at level 45, idx at level 45) : inject_scope.
Notation "'Load_i' dst ':=' ident '[' idx ']'" := (Sload Global (Op.Aglobal ident idx) (@nil positive) dst)(at level 60, ident at level 45, idx at level 45) : inject_scope.
Notation "'Store' dst ':=' src" := (Sstore false Global (Op.Aindexed Int.zero) (dst::(@nil positive)) src)(at level 60, dst at level 45) : inject_scope.
Notation "'ReleaseStore' dst ':=' src" := (Sstore false true (Op.Aindexed Int.zero) (dst::(@nil positive)) src)(at level 60, dst at level 45) : inject_scope.
Notation "'Store' dst '[' idx ']' ':=' src" := (Sstore false Global (Op.Aindexed idx) (dst::(@nil positive)) src)(at level 60, dst at level 45) : inject_scope.
Notation "'ReleaseStore' dst '[' idx ']' ':=' src" := (Sstore false true (Op.Aindexed idx) (dst::(@nil positive)) src)(at level 60, dst at level 45) : inject_scope.
Notation "'Store' dst '+' idx ':=' src" := (Sstore false Global (Op.Aindexed2 Int.zero) (dst::idx::(@nil positive)) src)(at level 60, dst at level 45, idx at level 45) : inject_scope.
Notation "'Store' dst '+' idx '×' sc '[' off ']' ':=' src" :=
  (Sstore false Global (Op.Aindexed2scaled sc off) (dst::idx::(@nil positive)) src)
    (at level 60, dst at level 45, idx at level 45, sc at level 45, off at level 45) : inject_scope.
Notation "'Store_g' ident ':=' src" := (Sstore false Global (Op.Aglobal ident Int.zero) (@nil positive) src)(at level 60) : inject_scope.
Notation "'ReleaseStore_g' ident ':=' src" := (Sstore false true (Op.Aglobal ident Int.zero) (@nil positive) src)(at level 60) : inject_scope.
Notation "'Store_g' ident '[' idx ']' ':=' src" := (Sstore false Global (Op.Abased ident Int.zero) (idx::(@nil positive)) src)(at level 60, idx at level 45) : inject_scope.
Notation "'Store_i' ident '[' idx ']' ':=' src" := (Sstore false Global (Op.Aglobal ident idx) (@nil positive) src)(at level 60, idx at level 45) : inject_scope.
Notation "'Store_s' soff ':=' src" := (Sstore false Global (Op.Ainstack soff) (@nil positive) src)(at level 60) : inject_scope.
Notation "'Cas' curr ':=' ptr ',' old '->' new" := (Satomicmem false Op.AScas (ptr::new::old::(@nil positive)) curr) (at level 60, old at next level) : inject_scope.

High level constructs.
Notation "'Assume' r1 '=' r2" := (Sassume (Op.Ccomp Ceq) (r1::r2::(@nil positive))) (at level 60, r1 at level 50, r2 at level 50) : inject_scope.
Notation "'Assume' r1 '==' imm" := (Sassume (Op.Ccompimm Ceq imm) (r1::(@nil positive))) (at level 60, r1 at level 50, imm at level 50) : inject_scope.
Notation "'Assume' r1 '≠' r2" := (Sassume (Op.Ccomp Cne) (r1::r2::(@nil positive))) (at level 60, r1 at level 50, r2 at level 50) : inject_scope.
Notation "'Assume' r1 '<>' imm" := (Sassume (Op.Ccompimm Cne imm) (r1::(@nil positive))) (at level 60, r1 at level 50, imm at level 50) : inject_scope.
Notation "'Assume' r1 '<' imm" := (Sassume (Op.Ccompimm Clt imm) (r1::(@nil positive))) (at level 60, r1 at level 50, imm at level 50) : inject_scope.

Notation " 'Atomic{' S '}' " := (Satomic true S) (at level 0, format " 'Atomic{' '//' S '//' '}' "): inject_scope.


Delimit Scope inject_scope with I.

Definition release (s:statement) : statement :=
  match s with
    | Satomicmem _ o args dst => Satomicmem true o args dst
    | Sstore _ ap ad args src => Sstore true ap ad args src
    | Sabort af r msg => Sabort af true msg
    | _ => s
  end.

Definition Local (s:statement) : statement :=
  match s with
    | Sload _ a args dst => Sload Local a args dst
    | Sstore r _ a args dst => Sstore r Local a args dst
    | _ => s
  end.


Section INJECTED_CODE.
Local Open Scope positive_scope.
Local Coercion Z_of_N : N >-> Z.
Local Coercion Zpos : positive >-> Z.
Local Coercion Z_of_nat : nat >-> Z.
Local Coercion Int.repr : Z >-> int.

Variable bi : backend_info.
Variable om : object_model.

Section LOCKING.
Non reentrant monitors.
  Notation mon := 1.
  Notation one := 2.
  Notation zero := 3.
  Notation old := 4.
  Notation curr := 5.

  Definition lock_statement : statement :=
    (
      Const zero := Int.zero;;
      Const one := Int.one;;
      Lea mon := mon[blk_mon];;
      Repeat
        Cas old := mon, zero -> one;;
        Move curr := old;;
        While curr Do Load curr := mon
      Until old = zero;;
      Sreturn nil
    )%I.

  Definition lock_high : statement :=
    (
      Atomic{
        Const zero := Int.zero;;
        Const one := Int.one;;
        Lea mon := mon[blk_mon];;
        Load old := mon;;
        Assume old = zero;;
        Store mon := one;;
        Sreturn nil
      }
    )%I.

  Definition unlock_statement : statement :=
    (
      Const zero := Int.zero;;
      Store mon[blk_mon] := zero;;
      Sfence false;;
      Sreturn nil
    )%I.

  Definition unlock_high : statement :=
    (
      Atomic{
        Const zero := Int.zero;;
        Store mon[blk_mon] := zero;;
        Sreturn nil
      }
    )%I.

  Definition lock_code :=
    Make_IC lock_statement lock_high (mon::nil).

  Definition unlock_code :=
    Make_IC unlock_statement unlock_high (mon::nil).

End LOCKING.

Marking.
Section Mark.
Code fragment to inject into another statement. The pointer held in register val, if not null, is stored in the bucket referenced by register bkt at offset given by register nw. Then register nw is incremented accordingly. This does not publish the marking.
  Variables bkt nw val : positive.

  Definition mark : statement :=
    (
      If val <> Int.zero
      Then (
        Leak LMark val 1024;;
        Local (Store bkt + nw := val);;
        Lea nw := nw[4%Z]
      ) Else Sskip
    )%I.

End Mark.

Section RootScan.
Code fragment to inject into another statement. base and greater registers must be unused in the calling code.
  Variables base md : positive.

  Definition frame := base.
  Notation bucket := (base + 1).
  Notation nw := (base + 2).
  Notation sz := (base + 3).
  Notation rt := (base + 4).

  Definition root_scan : statement :=
    (
      Local (Load frame := md[md_shadow]);;
      Lea bucket := md[md_bucket];;
      Const nw := Int.zero;;
      While frame Do (
        Local (Load sz := frame[hf_size]);;
        While sz Do (
          If nw ≥ bi.(bi_bucket_size)
          Then (Sseq (Sfence true) (Sabort Interleaved true Abort_RS))
          Else Sskip;;
          Lea sz := sz[(-4)%Z];;
          Local (Load rt := frame + sz [hf_roots]);;
          mark bucket nw rt
        );;
        Local (Load frame := frame[hf_next])
      );;
      Local (Store md[md_next_write] := nw)
    )%I.

End RootScan.

Section HANDSHAKE.
  Notation md := 1.
  Notation cd := 2.
  Notation phase_c := 3.
  Notation phase_m := 4.
  Notation col := 5.
  Notation stw := 6.

  Notation next := 8.

  Definition cooperate : statement :=
    (
      Sfreeperm;;
      Local (Load phase_m := md[md_phase]);;
      Lea_g cd := bi.(bi_collector);;
      Sfence false;;
      Load phase_c := cd[cd_phase];;
      If phase_m ≠ phase_c
      Then (
        If phase_m == ms_sync2
        Then (
          Local (Load col := cd[cd_mark_c]);;
          Local (Store md[md_alloc_c] := col);;
          root_scan next md
        )
        Else Sskip;;
        Store md[md_phase] := phase_c;;
        Sfence true;;
        Leak LHS md next
      )
      Else Srelease;;
      Sreturn nil
    )%I.

 Definition cooperate_high : statement :=
 (
   Sbranch (
     Atomic{
       Load 4 := 1 [md_phase];;
       Lea_i 2 := bi_collector bi [Int.zero];;
       Load 3 := 2 [cd_phase]
     } ;;
     Sbranch (
       Atomic{
         Assume 4 ≠ 3;;
         Assume 4 == ms_sync2;;
         Load 5 := 2 [cd_mark_c];;
         Store 1 [md_alloc_c]:=5;;
         Load frame 8 := 1 [md_shadow];;
         Lea 9 := 1 [md_bucket];;
         Const 10 := Int.zero;;
         While frame 8 <> Int.zero Do (
           Load 11 := frame 8 [hf_size];;
           While 11 <> Int.zero Do (
             If 10 ≥ bi.(bi_bucket_size)
             Then Sabort Atomic false Abort_RS
             Else Sskip;;
             Lea 11 := 11[(-4)%Z];;
             Load 12 := next + 11 [hf_roots];;
             If 12 <> Int.zero
             Then (
               Store 9 + 10 := 12;;
               Lea 10 := 10[4%Z]
             ) Else Sskip);;
           Load frame 8 := frame 8 [hf_next]);;
         Store 1 [md_next_write]:=10;;
         Store 1 [md_phase]:=3;;
         Sreturn nil
       } )
       Atomic{
      Assume 4 ≠ 3;;
      Assume 4 <> ms_sync2;;
      Store 1 [md_phase]:=3;;
      Sreturn nil
      } )%I
    Atomic{
   Load 4 := 1 [md_phase];;
   Lea_i 2 := bi_collector bi [Int.zero];;
   Load 3 := 2 [cd_phase];;
   Assume 4 = 3;;
   Sreturn nil
   } %I).

  Definition cooperate_code :=
    Make_IC cooperate cooperate_high (md::nil).

End HANDSHAKE.

Thread creation. To spawn a new thread, the parent first acquires an available slot in the mutator data array. The global lock mutator_lock protects such concurrent accesses to this array.
Section SPAWN.
  Variable func : Ast.ident.

  Notation param := 1.

  Notation pmd := (param + 1).
  Notation last := (pmd + 1).
  Notation zero := (last + 1).
  Notation one := (zero + 1).
  Notation c1 := (one + 1).
  Notation c2 := (c1 + 1).
  Notation fini := (c2 + 1).
  Notation md := (fini + 1).
  Notation status := (md + 1).
  Notation fp := (status + 1).
  Notation lock := (fp + 1).
  Notation curr := (lock + 1).

  Definition spawn_statement : statement :=
    ( Sfreeperm;;
      Lea_g lock := bi.(bi_mutator_lock);;
      Const zero := Int.zero;;
      Const one := Int.one;;
      Repeat
        Cas last := lock, zero -> one;;
        Move curr := last;;
        While curr Do Load curr := lock
      Until last = zero;;

      Lea_g pmd := bi.(bi_mutator_data);;
      Lea_i last := bi.(bi_mutator_data)[md_size bi];;
      Const md := Int.zero;;
      Const curr := Int.zero;;
      Repeat
        Local (Load status := pmd[md_status]);;
        If status == ms_available
        Then Move md := pmd
        Else Sskip;;
        Lea pmd := pmd[sizeof_md bi];;
        Cmp c1 := pmd = last;;
        Cmp c2 := md ≠ zero;;
        Lea fini := c1 + c2
      Until fini;;

      If md = zero
      Then (Sfence true;; Sabort Interleaved true Abort_Spawn)
      Else Sskip;;
      Lea_g fp := func;;
      Local (Store md[md_fp] := fp);;
      Local (Store md[md_arg] := param);;
      Const status := ms_quick;;
      Local (Store md[md_status] := status);;

      Const zero := Int.zero;;
      Store_g bi.(bi_mutator_lock) := zero;;
      Sfence true;;
      Leak LSpawn md zero;;
      Lea_g fp := bi.(bi_thread_main);;
      Sreturn (fp::md::nil)
    )%I.

  Definition spawn_statement_high : statement :=
    (
      Atomic{
        Lea_i lock := bi_mutator_lock bi [Int.zero];;
        Const zero := Int.zero;;
        Const one := Int.one;;
        Load last := lock [Int.zero];;
        Assume last = zero;;
        Store lock [Int.zero]:=one
      } ;;

      Atomic{
        Lea_i pmd := bi_mutator_data bi [Int.zero];;
        Lea_i last := bi_mutator_data bi [md_size bi];;
        Const md := Int.zero;;
        Const curr := Int.zero;;
        Repeat
          Load status := pmd [md_status];;
          If status == ms_available Then Move md := pmd Else Sskip;;
          Lea pmd := pmd [sizeof_md bi];;
          Cmp c1 := pmd = last;;
          Cmp c2 := md ≠ zero;;
          Lea fini := c1 + c2
        Until fini;;
        If md = zero Then Sskip;; Sabort Atomic false Abort_Spawn Else Sskip;;
        Lea_i fp := func [Int.zero];;
        Store md [md_fp] := fp;;
        Store md [md_arg]:= param;;
        Const status := ms_quick;;
        Store md [md_status]:= status;;
        Const zero := Int.zero;;
        Store_g bi_mutator_lock bi := zero;;
        Lea_i fp := bi_thread_main bi [Int.zero];;
        Sreturn (fp :: md :: nil)
      }
    )%I.

  Definition spawn_code : injected_body :=
    Make_IC spawn_statement spawn_statement_high (param::nil).

End SPAWN.

Instrumented body of a thread. A newly spawned thread waits for the collector to update its status from quick to async. A dying thread releases its mutator data slot.
Section THREAD_MAIN.
Section START.

  Notation param := 1.
  Notation st := 2.
  Notation fp := 3.
  Notation arg := 4.
  Definition start_statement : statement :=
    ( Sfreeperm;;
      Local (Load fp := param[md_fp]);;
      Local (Load arg := param[md_arg]);;
      Sfence false;;
      Repeat
        Load st := param[md_status]
      Until st == ms_running;;
      Srelease;;
      Sreturn (fp::arg::nil)
    )%I.

  Definition start_statement_high : statement :=
    (
      Atomic{
        Load fp := param[md_fp];;
        Load arg := param[md_arg];;
        Load st := param[md_status];;
        Assume st == ms_running;;
        Sreturn (fp::arg::nil)
      }
    )%I.

  Definition start_code : injected_body :=
    Make_IC start_statement start_statement_high (param::nil).

End START.

Section END.
  Notation param := 1.
  Notation st := 2.
  Notation curr := 4.
  Notation zero := 6.
  Notation one := 7.
  Notation lock := 8.
  Notation last := 9.
  Definition end_statement : statement :=
    ( Sfreeperm;;
      Lea_g lock := bi.(bi_mutator_lock);;
      Const zero := Int.zero;;
      Const one := Int.one;;
      Repeat
        Cas last := lock, zero -> one;;
        Move curr := last;;
        While curr Do Load curr := lock
      Until last = zero;;

      Const st := ms_available;;
      Local (Store param[md_status] := st);;
      Store lock := zero;;
      Sfence true;;
      Const curr := Int.zero;;

      Sreturn nil
    )%I.

  Definition end_statement_high : statement :=
    (
      Atomic{
        Lea_g lock := bi.(bi_mutator_lock);;
        Const zero := Int.zero;;
        Const one := Int.one;;
        Load last := lock;;
        Assume last = zero;;
        Store lock := one
      };;
      Atomic{
        Const st := ms_available;;
        Store param[md_status] := st;;
        Store lock := zero;;
        Sreturn nil
      }
    )%I.

  Definition end_code : injected_body :=
    Make_IC end_statement end_statement_high (param::nil).

End END.

  Definition thread_main_sig : Ast.signature :=
    Ast.mksignature (Ast.Tint::Ast.Tint::nil) (Some Ast.Tint).

  Notation tid := 1.
  Notation fp := 2.
  Notation arg := 3.
  Notation res := 4.

  Definition thread_main : code :=
    of_pair_list
      ((1, Iinject start_code (tid::nil) (fp::arg::nil) 2)
     ::(2, Icall thread_main_sig (inl _ fp) (tid::arg::nil) res 3)
     ::(3, Iinject end_code (tid::nil) nil 4)
     ::(4, Ireturn tid)
     ::nil).

  Definition thread_main_func : function :=
    mkfunction (Ast.mksignature (Ast.Tint::nil) (Some Ast.Tint))
    (tid::nil) Int.zero
    thread_main
    1.

End THREAD_MAIN.

Handling of roots.
Section ROOTS.
  Variable max_roots : N.

  Notation md := 1.
  Notation sz := 2.
  Notation top := 3.
  Notation rt := 4.
  Notation zero:= 5.
  Notation hf := 6.

Prologue: at function entry, allocate a Henderson frame and push it on the shadow stack.
  Definition prologue : statement :=
    ( Sfreeperm;;
      Lea_s hf := Int.zero;;
      Const sz := Int.shl max_roots (Int.repr 2);;
      Local (Store hf[hf_size] := sz);;
      Local (Load top := md[md_shadow]);;
      Local (Store hf[hf_next] := top);;
      Const rt := hf_roots;;
      Const zero := Int.zero;;
      Repeat
        Local (Store hf + rt := zero);;
        Lea rt := rt[4%Z]
      Until rt == Int.add hf_roots (Int.shl max_roots 2%Z);;
      Store md[md_shadow] := hf;;
      Sfence false;;
      Srelease;;
      Sreturn nil
    )%I.

  Definition prologue_high : statement :=
    (
      Atomic{
        Lea_s hf := Int.zero;;
        Const sz := Int.shl max_roots (Int.repr 2);;
        Store hf [hf_size]:=sz;;
        Load top := 1 [md_shadow];;
        Store hf [hf_next]:=top;;
        Const rt := hf_roots;;
        Const zero := Int.zero;;
        Repeat
          Store hf + rt := zero;;
          Lea rt := rt [Int.repr 4]
        Until rt == Int.add hf_roots (Int.shl max_roots (Int.repr 2));;
        Store 1 [md_shadow] := hf;;
        Sreturn nil
      }
    )%I.

  Definition prologue_code :=
    Make_IC prologue prologue_high (md::nil).

Epilogue: on return, pop a frame from the shadow stack (automatically freed).
  Definition epilogue : statement :=
    ( Sfreeperm;;
      Local (Load_s top := hf_next);;
      Store md[md_shadow] := top;;
      Sfence true;;
      Sreturn nil
    )%I.

  Definition epilogue_high : statement := (
    Atomic{
      Load_s top := hf_next;;
      Store md[md_shadow] := top;;
      Sreturn nil
    })%I.

  Definition epilogue_code :=
    Make_IC epilogue epilogue_high (md::nil).

Copy a register in the corresponding slot of the shadow stack.
  Definition saveref (slot: N) (rt: positive) : statement :=
    (
      Local (Store_s (Int.add (slot * 4)%Z hf_roots) := rt)
    )%I.

  Definition slot_of_reg (r: positive) : N := N_of_Z (Zpos r - 1).

  Definition saveref_code (rt: positive) :=
    Make_IC (saveref (slot_of_reg rt) rt;; Sreturn (rt::nil))%I
            (Satomic false (saveref (slot_of_reg rt) rt;;Sreturn (rt::nil)))%I
            (rt::nil).

End ROOTS.

Write barrier.
Section WRITEBARRIER.
  Notation md := 1.
  Notation obj := 2.
  Notation val := 3.

  Notation phase := 4.
  Notation bucket := 9.
  Notation nw := 10.
  Notation old := 11.

  Definition update_stmt (fld: int) : statement :=
    (
      Local (Load phase := md[md_phase]);;
      If phase <> ms_async
      Then (
        (Sfence false;;
         (Load old := obj[fld]));;
        Lea bucket := md[md_bucket];;
        Local (Load nw := md[md_next_write]);;
        If nw ≥ (Int.sub bi.(bi_bucket_size) (Int.repr 8))
        Then (Sabort Interleaved false Abort_WB)
        Else (
          mark bucket nw old;;
          mark bucket nw val;;
          Store md[md_next_write] := nw;;
          Sfence true
        )
      ) Else Sskip;;
      Store obj[fld] := val;;
      Sfence true
    )%I.

Definition update_stmt_high fld :=
  (
    Sbranch (Sabort Interleaved false Abort_WB) (
      Sbranch (
        Atomic{
          Local (Load phase := md [md_phase]);;
          Assume phase <> ms_async;;
          Load old := obj [fld]
        } ;;
        Atomic{
          Lea bucket := md [md_bucket];;
          Local (Load nw := md [md_next_write]);;
          Assume nw < Int.sub (Common.bi_bucket_size bi) (Int.repr 8);;
          mark bucket nw old;;
          mark bucket nw val;;
          release (Store md[md_next_write] := nw)
        } ;;
        Atomic{ release (Store obj [fld]:=val) })%I

        Atomic{
           Local (Load phase := md [md_phase]);;
           Assume phase == ms_async;;
           release (Store obj [fld]:=val)
        }))%I.

  Definition write_stmt (f: field) : statement :=
    let fld : int := offset_of_field f in
      ((if is_ptr_field f
       then update_stmt fld
       else Store obj[fld] := val);;
      if is_field_volatile f
      then Sfence false;; Sreturn nil
      else Sreturn nil)%I
  .

  Definition write_stmt_high (f: field) : statement :=
    let fld : int := offset_of_field f in
    let fence : bool := is_field_volatile f in
      (if is_ptr_field f
       then update_stmt_high fld
       else Satomic fence ((Store obj[fld] := val);; Sreturn nil))%I
  .

  Definition read_int_stmt (slot: N) (f: field) : statement :=
    let fld : int := offset_of_field f in
      (
      Load val := obj[fld];;
      Sreturn (val::nil)
      )%I.

  Definition read_ptr_stmt (slot: N) (f: field) : statement :=
    let fld : int := offset_of_field f in
      (
     Load val := obj[fld];;
      saveref slot val;;
      Sreturn (val::nil)
      )%I.

  Definition write_code f := Make_IC (write_stmt f) (write_stmt_high f) (md::obj::val::nil).
  Definition read_code s f :=
    if is_ptr_field f
    then Make_IC (read_ptr_stmt s f) (Atomic{ read_ptr_stmt s f})%I (obj::nil)
    else Make_IC (read_int_stmt s f) (Atomic{ read_int_stmt s f})%I (obj::nil)
  .

End WRITEBARRIER.

Global variables.
Section GLOBALS.
  Variable base : Ast.ident.
  Variable offset : Z.
  Variable kind : field_kind.

  Notation val := 1.

  Definition rg_stmt : statement :=
    (
      Load_i val := base [ offset ];;
      Sreturn (val::nil)
    )%I.

  Definition rg_stmt_v : statement :=
    (
      Sfence false;;
      Load_i val := base [ offset ];;
      Sreturn (val::nil)
    )%I.

  Definition wg_stmt : statement :=
    (
      Store_i base [ offset ] := val;;
      Sreturn nil
    )%I.

  Definition wg_stmt_v : statement :=
    (
      Store_i base [ offset ] := val;;
      Sfence false;;
      Sreturn nil
    )%I.

  Definition read_global_code :=
    if is_volatile kind
    then Make_IC rg_stmt_v (Atomic{ rg_stmt })%I nil
    else Make_IC rg_stmt (Satomic false rg_stmt) nil.

  Definition write_global_code :=
    if is_volatile kind
    then Make_IC wg_stmt_v (Atomic{ wg_stmt })%I (val::nil)
    else Make_IC wg_stmt (Satomic false wg_stmt) (val::nil).

End GLOBALS.

Allocation.
Section TREIBER_ALLOC.
  Variable slot : N.
  Variable header : int.

  Notation md := 1.
  Notation flptr:= 3.
  Notation curr := 4.
  Notation head := 5.
  Notation next := 6.
  Notation tag := 7.
  Notation color := 8.
  Notation h := 9.

  Definition new_statement : statement :=
    ( Sfreeperm;;
      Lea_g flptr := bi.(bi_free_list);;
      Load curr := flptr;;
      Repeat
        Move head := curr;;
        If head == Int.zero
        Then (Sseq (Sfence true) (Sabort Interleaved true Abort_OOM))
        Else Sskip;;
        Local (Load next := head[blk_next]);;
        release (Cas curr := flptr, head -> next)
      Until curr = head;;
      Const h := header;;
      Local (Store head[blk_hdr] := h);;
      Leak LAlloc head h;;
      saveref slot head;;
      Local (Load color := md[md_alloc_c]);;
      Store head[blk_color] := color;;
      Sfence true;;
      Sreturn (head::nil)
    )%I.

  Definition new_statement_high : statement :=
    (Sbranch (Sabort Interleaved false Abort_OOM)
       (Atomic{
            Lea_i flptr := Common.bi_free_list bi[Int.zero];;
            Load head := flptr;;
            Move curr := head;;
            Assume head <> Int.zero;;
            Load next := head[blk_next];;
            Store flptr[Int.zero]:= next
            } ;;
        Atomic{
            Const h := header;;
            Store head[blk_hdr]:=h;;
            Store_s Int.add (Int.repr (Z_of_N slot * 4)) hf_roots := head;;
            Load color := md[md_alloc_c];;
            Store head[blk_color]:=color;;
            Sreturn (head::nil)
            }
       ))%I.

  Definition new_code : injected_body :=
    Make_IC new_statement new_statement_high (md::nil).

End TREIBER_ALLOC.

End INJECTED_CODE.

Generated by coq2html