Module GCthread

Require Import Coqlib Integers Maps.
Require Import Registers.

Require Import RTLinject MIR DataStructures Common.

Require Import INJECT InjectedCode.

Local Open Scope positive_scope.
Local Open Scope inject_scope.

Section GCTHREAD.
  Variable bi : backend_info.
  Variable om : object_model.
  Variable p : program.
  Variable max_p: Z. (* size of the array of global pointer variables *)

  Notation r := 1.
  Notation fini := 2.
  Notation rc := 3.
  Notation md := 4.
  Notation last := 5.
  Notation st := 6.
  Notation f := 7.
  Notation cc := 8.
  Notation mc := 9.
  Notation cd := 10.
  Notation rt := 11.
  Notation top := 12.
  Notation bucket := 13.
  Notation nw := 14.
  Notation nr := 15.
  Notation pnr := 16.
  Notation b := 17.
  Notation tag := 18.
  Notation hdr := 19.
  Notation sfls := 20.
  Notation sfle := 21.
  Notation flptr :=22.
  Notation curr := 23.
  Notation head := 24.
  Notation clean:= 25.
  Notation pfld := 26.
  Notation lfld := 27.
  Notation next := 28.

  Notation rmax := 64. (* write-only local variable. *)

Section HANDSHAKE.
  Variable fld : int.
  Variable val : int.
  Definition wait_hs : statement :=
    Sfreeperm;;
    Repeat
      Const rc := Int.zero;;
      Const fini := Int.one;;
      Lea_g md := bi.(bi_mutator_data);;
      Lea_i last := bi.(bi_mutator_data)[md_size bi];;
      Sfence false;;
      Repeat
        Sfence false;;
        Load st := md[md_status];;
        If st <> ms_available
        Then (
          Lea rc := rc [ Int.one ];;
          If st <> ms_quick
          Then (
            Sfence false;;
            Load f := md[fld];;
            If f == val
            Then Sskip
            Else Const fini := Int.zero
          )
          Else Sfence false
        )
        Else Sfence false;;
        Lea md := md[sizeof_md bi]
      Until md = last;;
      If rc == Int.zero
      Then Sfence true;; Sreturn nil
      Else Sfence false
    Until fini;;
    Srelease.

  Definition wait_hs_high :=
    Repeat
      Atomic{
      Const rc := Int.zero;;
      Const fini := Int.one;;
      Lea_g md := bi.(bi_mutator_data);;
      Lea_i last := bi.(bi_mutator_data)[md_size bi]
      };;
      Repeat
        Atomic{ Load st := md[md_status] };;
        Atomic{
          If st <> ms_available
          Then (
            Lea rc := rc [ Int.one ];;
            If st <> ms_quick
            Then (
              Load f := md[fld];;
              If f == val
              Then Sskip
              Else Const fini := Int.zero
            )
            Else Sskip
          )
          Else Sskip;;
          Lea md := md[sizeof_md bi]
        }
      Until md = last;;
      Atomic{
        If rc == Int.zero
        Then Sreturn nil
        Else Sskip
      }
    Until fini.

End HANDSHAKE.

  Definition mark_grey (b: reg) : statement :=
    Local (Load tag := b[blk_color]);;
    If tag = cc
    Then (
      If top ≥ bi.(bi_collector_stack_size)
      Then (Sfence true;; Sabort Interleaved true Abort_OCS)
      Else Sskip;;
      Local (Store_g bi.(bi_collector_stack)[top] := b);;
      Lea top := top[Int.repr 4%Z]
    ) Else Sskip.

  Definition empty_collector_stack : statement :=
    While top <> Int.zero Do (
      Lea top := top[Int.repr (-4)%Z];;
      Local (Load_g b := bi.(bi_collector_stack)[top]);;
      Sfence false;;
      Load tag := b[blk_color];;
      If tag ≠ mc
      Then (
        Local (Load hdr := b[blk_hdr]);;
        Leak LGrey b rmax;;
        Const f := Int.zero;;
        Sfence false;;
        While f <> Int.repr (Zpos om.(om_object_size)) Do (
          om.(om_is_field_pointer_stmt) hdr f r;;
          If r <> Int.zero
          Then (
            Sfence false;;
            Load r := b + f × Int.repr 4 [blk_first_field];;
            If r <> Int.zero
            Then (
              mark_grey r
            ) Else Sskip;;
            Sfence false
          ) Else Sskip ;;
          Lea f := f[Int.one]
        );;
        Store b[blk_color] := mc
      ) Else Sskip
    ).

  Definition trace : statement :=
      Repeat
        Const clean := Int.one;;
        Lea_g md := bi.(bi_mutator_data);;
        Lea_i last := bi.(bi_mutator_data)[md_size bi];;
        Sfence false;;
        Repeat
          Lea bucket := md[md_bucket];;
          Local (Load nr := md[md_next_read]);;
          Sfence false;;
          Load nw := md[md_next_write];;
          While nr ≠ nw Do (
            Const clean := Int.zero;;
            Local (Load b := bucket + nr [Int.zero]);;
            Leak LGrey b rmax;;
            Lea nr := nr[Int.repr 4];;
            mark_grey b;;
            Sfence false;;
            empty_collector_stack
          );;
          Store md[md_next_read] := nr;;
          Sfence true;;
          Lea md := md[sizeof_md bi]
        Until md = last
      Until clean.

 Definition trace_high : statement :=
   Repeat
     Atomic{
       Const clean := Int.one;;
       Lea_i md := bi_mutator_data bi [Int.zero];;
       Lea_i last := bi_mutator_data bi [md_size bi]
     } ;;
     Repeat
       Atomic{
         Lea bucket := md [md_bucket];;
         Local (Load nr := md [md_next_read]);;
         Load nw := md [md_next_write]
         } ;;
         While nr ≠ nw Do (
           Atomic{
             Const clean := Int.zero;;
             Local (Load b := bucket + nr [Int.zero]);;
             Leak LGrey b rmax;;
             Lea nr := nr [Int.repr 4];;
             Local (Load tag := b [blk_color]);;
             If tag = cc
             Then If top ≥ bi_collector_stack_size bi
                  Then (Srelease;; Sabort Atomic true MIR.Abort_OCS) Else Sskip;;
                  Local (Store_g bi_collector_stack bi [top]:=b);;
                  Lea top := top [Int.repr 4]
             Else Sskip
           } ;;
           While top <> Int.zero Do (
             Atomic{
               Lea top := top [Int.repr (-4)];;
               Local (Load_g b := bi_collector_stack bi [top]);;
               Load tag := b [blk_color]
             } ;;
             If tag ≠ mc
             Then
               Atomic{
                 Local (Load hdr := b [blk_hdr]);;
                 Leak LGrey b rmax;;
                 Const f := Int.zero
               } ;;
               While f <> Int.repr (Zpos (om_object_size om)) Do
                 Sbranch (
                   Atomic{
                     om.(om_is_field_pointer_stmt) hdr f r;;
                     Assume r <> Int.zero;;
                     Load r := b + f × Int.repr 4 [blk_first_field]
                   } ;;
                   Atomic{
                     If r <> Int.zero
                     Then Local (Load tag := r [blk_color]);;
                          If tag = cc
                          Then If top ≥ bi_collector_stack_size bi
                               Then (Srelease;; Sabort Atomic true MIR.Abort_OCS) Else Sskip;;
                               Local (Store_g bi_collector_stack bi [top]:=r);;
                               Lea top := top [Int.repr 4]
                          Else Sskip
                     Else Sskip;;
                     Lea f := f [Int.one]
                   })
                   ( om.(om_is_field_pointer_stmt) hdr f r;;
                     Assume r == Int.zero;;
                     Lea f := f [Int.one]
                    );;
                    Store b [blk_color] := mc
               Else Sskip));;
       Atomic{
         release (Store md [md_next_read]:=nr);;
         Lea md := md [sizeof_md bi]
       }
     Until md = last
   Until clean.

  Definition clear_fields : statement :=
    Lea pfld := b[blk_first_field];;
    Lea lfld := b[object_byte_size om];;
    While pfld ≠ lfld Do (
      Local (Store pfld := r);;
      Lea pfld := pfld [ Int.repr 4 ]
    ).

  Definition sweep : statement :=
    Lea_g b := bi.(bi_heap);;
    Lea_i last := bi.(bi_heap)[heap_byte_size om];;
    Const sfls := Int.zero;;
    Const sfle := Int.zero;;
    Sfence false;;
    Repeat
      Load tag := b[blk_color];;
      If tag = cc
      Then (
        Leak LFree b rmax;;
        Const r := color_blue;;
        Local (Store b[blk_color] := r);;
        Const r := Int.zero;;
        clear_fields;;
        If sfle == Int.zero
        Then Move sfle := b
        Else Sskip;;
        Local (Store b[blk_next] := sfls);;
        Move sfls := b
      ) Else Sskip;;
      Lea b := b [object_byte_size om];;
      Sfence false
    Until b = last;;
    If sfle <> Int.zero
    Then (
      Lea_g flptr := bi.(bi_free_list);;
      Sfence false;;
      Load curr := flptr;;
      Repeat
        Move head := curr;;
        Lea next := sfle[blk_next];;
        Local (Store next := head);;
        release (Cas curr := flptr, head -> sfls)
      Until curr = head
    ) Else Sskip.

  Definition sweep_high :=
    Atomic{
       Lea_i b := bi_heap bi [Int.zero];;
       Lea_i last := bi_heap bi [heap_byte_size om];;
       Const sfls := Int.zero;;
       Const sfle := Int.zero
     } ;;
     Repeat
       Load tag := b [blk_color];;
       Atomic{
         If tag = cc
         Then Leak LFree b rmax;;
              Const r := color_blue;;
              Local (Store b [blk_color]:=r);;
              Const r := Int.zero;;
              clear_fields;;
              If sfle == Int.zero Then Move sfle := b Else Sskip;;
              Local (Store b [blk_next]:=sfls);;
              Move sfls := b Else Sskip;;
         Lea b := b [object_byte_size om]
       }
     Until b = last;;
     If sfle <> Int.zero
     Then
       Atomic{
         Lea_i flptr := bi_free_list bi [Int.zero];;
         Load curr := flptr [Int.zero]
       } ;;
       Sloop
         Atomic{
           Move head := curr;;
           Lea next := sfle [blk_next];;
           Local (Store next [Int.zero]:=head);;
           Load curr := flptr[Int.zero];; Srelease;;
           Assume curr ≠ head
         };;
       Atomic{
         Move head := curr;;
         Lea next := sfle [blk_next];;
         Local (Store next [Int.zero]:=head);;
         Load curr := flptr[Int.zero];;
         Assume curr = head;;
         release (Store flptr[Int.zero]:=sfls)
       }
     Else Sskip.

  Definition cycle : statement :=
    Const r := ms_sync1;;
    Store cd[cd_phase] := r;;
    wait_hs md_phase ms_sync1;;

    Const r := ms_sync2;;
    Store cd[cd_phase] := r;;
    wait_hs md_phase ms_sync2;;

    Const r := ms_async;;
    Store cd[cd_phase] := r;;

    Lea_g pnr := bi.(bi_ptr_globals);;
    Lea last := pnr[Int.repr max_p];;
    While pnr ≠ last Do (
      Load rt := pnr;;
      If rt <> Int.zero
      Then (
        Local (Store_g bi.(bi_collector_stack)[top] := rt);;
        Lea top := top[Int.repr 4%Z]
      ) Else Sskip;;
      Lea pnr := pnr [Int.repr 4%Z]
    );;

    wait_hs md_phase ms_async;;

    trace;;

    sweep
    .

  Definition cycle_high :=
    Atomic{
      Const r := ms_sync1;;
      Store cd [cd_phase]:=r
      } ;;
      wait_hs_high md_phase ms_sync1;;
       Atomic{
      Const r := ms_sync2;;
      Store cd [cd_phase]:=r
      } ;;
      wait_hs_high md_phase ms_sync2;;
       Atomic{
      Const r := ms_async;;
      Store cd [cd_phase]:=r
      } ;;
      Atomic{
       Lea_i pnr := bi_ptr_globals bi [Int.zero];;
       Lea last := pnr [Int.repr 1]};;
      While pnr ≠ last
      Do (Atomic{
          Load rt := pnr [Int.zero]
          } ;;
          Atomic{
          If rt <> Int.zero
          Then Local (Store_g bi.(bi_collector_stack)[top] := rt);;
               Lea top := top [Int.repr 4] Else Sskip;;
          Lea pnr := pnr [Int.repr 4]});;
      wait_hs_high md_phase ms_async;;
      trace_high;;
      sweep_high.

  Definition let_threads_go : statement :=
    Lea_g md := bi.(bi_mutator_data);;
    Lea_i last := bi.(bi_mutator_data)[md_size bi];;
    Repeat
      Const r := Int.zero;;
      Local (Store md[md_next_read] := r);;
      release (Load st := md[md_status]);;
      If st == ms_quick
      Then (
        Local (Store md[md_alloc_c] := cc);;
        Const r := ms_async;;
        Local (Store md[md_phase] := r);;
        Const r := ms_running;;
        Store md[md_status] := r;;
        Sfence true
      ) Else Sskip;;
      Lea md := md[sizeof_md bi]
    Until md = last.

  Definition let_threads_go_high :=
    Atomic{
      Lea_i md := bi_mutator_data bi [Int.zero];;
      Lea_i last := bi_mutator_data bi [md_size bi]
      } ;;
      Repeat
        Atomic{
             Const r := Int.zero;;
             Local (Store md [md_next_read]:=r);;
             release (Load st := md[md_status])
             } ;;
              Atomic{
             If st == ms_quick
             Then Local (Store md [md_alloc_c]:=cc);;
                  Const r := ms_async;;
                  Local (Store md [md_phase]:=r);;
                  Const r := ms_running;;
                  Store md [md_status]:=r;;
                  Sfence true Else Sskip;;
      Lea md := md [sizeof_md bi]
    }
    Until md = last.

  Definition gc_startup : statement :=
    Sfreeperm;;
    Lea_g cd := bi.(bi_collector);;
    Const r := ms_async;;
    Local (Store cd[cd_phase] := r);;
    Lea_g pnr := bi.(bi_heap);;
    Local (Store_g bi.(bi_free_list) := pnr);;
    Lea_i last := bi.(bi_heap)[Int.sub (heap_byte_size om) (object_byte_size om)];;
    Const tag := color_blue;;
    Repeat
      Lea b := pnr[object_byte_size om];;
      Local (Store pnr[blk_next] := b);;
      Local (Store pnr[blk_color] := tag);;
      Move pnr := b
    Until pnr = last;;
    Lea_g r := p.(prog_entry);;
    Lea_g pnr := bi.(bi_mutator_data);;
    Local (Store pnr[md_fp] := r);;
    Const r := ms_quick;;
    Store pnr[md_status] := r;;
    Sfence true;;
    Lea_g r := bi.(bi_thread_main);;
    Leak LSpawn pnr rmax;;
    Sreturn (r::pnr::nil).

  Definition gc_startup_high : statement :=
    Atomic{
      Lea_g cd := bi.(bi_collector);;
      Const r := ms_async;;
      Store cd[cd_phase] := r;;
      Lea_g pnr := bi.(bi_heap);;
      Store_g bi.(bi_free_list) := pnr;;
      Lea_i last := bi.(bi_heap)[Int.sub (heap_byte_size om) (object_byte_size om)];;
      Const tag := color_blue;;
      Repeat
        Lea b := pnr[object_byte_size om];;
        Store pnr[blk_next] := b;;
        Store pnr[blk_color] := tag;;
        Move pnr := b
      Until pnr = last;;
      Lea_g r := p.(prog_entry);;
      Lea_g pnr := bi.(bi_mutator_data);;
      Store pnr[md_fp] := r;;
      Const r := ms_quick;;
      Store pnr[md_status] := r;;
      Lea_g r := bi.(bi_thread_main);;
      Leak LSpawn pnr rmax;;
      Sreturn (r::pnr::nil)
    }.

  Definition gc_main : statement :=
    Const top := Int.zero;;
    Const cc := color_BW;;
    Xor mc := cc ^ color_mask;;
    (Store cd[cd_mark_c] := mc);;
    Repeat
      let_threads_go;;
      cycle;;
      Local (Load cc := cd[cd_mark_c]);;
      Xor mc := cc ^ color_mask;;
      release (Store cd[cd_mark_c] := mc);;
      Const r := Int.zero
    Until r.

  Definition gc_high :=
    Atomic{
      Const top := Int.zero;;
      Const cc := color_BW;;
      Xor mc := cc ^ color_mask;;
      Store cd [cd_mark_c]:=mc
    } ;;
    Repeat
      let_threads_go_high;;
      cycle_high;;
      Atomic{
        Local (Load cc := cd [cd_mark_c]);;
        Xor mc := cc ^ color_mask;;
        release (Store cd [cd_mark_c]:=mc);;
        Const r := Int.zero
      }
    Until r.

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

  Definition gc_main_func : RTLinject.function :=
    RTLinject.mkfunction gc_main_sig nil Int.zero
    (of_pair_list
        ((1, Iinject (Make_IC gc_startup gc_startup_high nil) nil (r::pnr::nil) 2)
       ::(2, Ithreadcreate r pnr 3)
       ::(3, Iinject (Make_IC gc_main gc_main nil) nil nil 4)
       ::(4, Ireturn xH)
       ::nil))
    1.

End GCTHREAD.