Require Import Coqlib Maps.
Require Import mathcomp.ssreflect.fintype.
Require Import AST Values Globalenvs.
Require Import Blockset GMemory MemClosures MemAux InteractionSemantics GAST Injections.
Require Import Lists.Streams Lia.

Definitions of global runtime states

Definition tid : Type := positive.
Definition fid : Type := positive.
Definition mid : Type := nat.

The freelists of all threads and runtime modules

Module FLists.

  
  Record t: Type :=
    { flist_content: fid -> freelist;
      thread_flmap: tid -> nat -> fid;
    }.

  Record wd (fls: t) : Prop :=
    {
      flist_norep: forall f, norep (flist_content fls f);
      flist_disj: forall f1 f2, f1 <> f2 ->
                                disj (flist_content fls f1) (flist_content fls f2);
      thread_fl_norep: forall t n1 n2, n1 <> n2 ->
                                       thread_flmap fls t n1 <>
                                       thread_flmap fls t n2;
      thread_fl_disj: forall t1 t2 n1 n2, t1 <> t2 ->
                                          (thread_flmap fls t1 n1) <>
                                          (thread_flmap fls t2 n2);
    }.

Initial Freelists

  Definition fid_to_freelist_func (base: block) (fid: positive) (n: nat) : block :=
    let: row := (Pos.to_nat fid - 1)%nat in
    let: col := n in
    (Pos.of_nat ((row + col + 2) * (row + col + 1) / 2 - col)%nat + base - 1)%positive.

  Lemma arith_result2:
    forall m n,
      ((m + n + 2) * (m + n + 1) / 2 > n)%nat .

  Lemma div2_plus_1:
    forall y x:nat, (x / 2 - y = (x - 2 * y) / 2)%nat.

  
  Lemma arith_aux:
    forall x1 y1 x2 y2, (x1 + y1 < x2 + y2 ->
                   (x1 + y1 + 2) * (x1 + y1 + 1) / 2 - y1 <
                   (x2 + y2 + 2) * (x2 + y2 + 1) / 2 - y2)%nat.
    
    
  Lemma arith_result1:
    forall m1 n1 m2 n2,
      m1 <> m2 \/ n1 <> n2 ->
      ((m1 + n1 + 2) * (m1 + n1 + 1) / 2 - n1)%nat <>
      ((m2 + n2 + 2) * (m2 + n2 + 1) / 2 - n2)%nat.
      
  
  
  CoFixpoint func_to_stream {A: Type} (func: nat -> A) (base: nat): Stream A :=
    Cons (func base) (func_to_stream func (S base)).


  Definition frob {A: Type} (s: Stream A) : Stream A :=
    match s with
    | Cons h t => Cons h t
    end.
  
  Theorem frob_eq: forall A (s: Stream A), s = frob s.
      
  Lemma freelist_func_stream_S:
    forall A n (func: nat -> A) base,
      Str_nth (S n) (func_to_stream func base) =
      Str_nth n (func_to_stream func (S base)).
    
  Lemma freelist_func_stream_eq:
    forall A n (func: nat -> A) base,
      Str_nth n (func_to_stream func base) = func (n + base)%nat.
  
    
  Definition init_flist_content (base: block) : fid -> freelist :=
    fun f: fid =>
      func_to_stream (fid_to_freelist_func base f) 0.
      

  Lemma init_freelist_norep:
    forall base f, norep (init_flist_content base f).

  Lemma init_freelist_disj:
    forall base f1 f2, f1 <> f2 -> disj (init_flist_content base f1) (init_flist_content base f2).
    
  Definition tid_to_fid_stream (i: tid) (n: nat) : fid :=
    let: row := (Pos.to_nat i - 1)%nat in
    let: col := n in
    Pos.of_nat ((row + col + 2) * (row + col + 1) / 2 - col)%nat.


  Lemma tid_to_fid_stream_disj:
    forall i1 i2 n1 n2,
      i1 <> i2 \/ n1 <> n2 ->
      tid_to_fid_stream i1 n1 <> tid_to_fid_stream i2 n2.

  Definition init: block -> t :=
    fun base : block => Build_t (init_flist_content base) tid_to_fid_stream.
        
  Theorem init_wd:
    forall b, wd (init b).


  Definition get_block (fl: freelist) (n: nat) : block := Str_nth n fl.
  Definition get_fl (x: t) (f:fid) : freelist := x.(flist_content) f.
  
  Definition get_tfid (x: t) (i: tid) (n: nat) : fid := (x.(thread_flmap) i n).

  Definition get_tfl (x: t) (i: tid) (n: nat) : freelist := get_fl x (get_tfid x i n).

  Definition get_tfblock (x: t) (i: tid) (n: nat) (bid: nat) : block :=
    get_block (get_tfl x i n) bid.

  Definition bbelongsto (x: t) (i: tid) (b: block) : Prop :=
    exists n bid, get_tfblock x i n bid = b.

  Definition fbelongsto (x: t) (i: tid) (f: fid) : Prop :=
    exists n, get_tfid x i n = f.

  Definition bbelongstof (x: t) (f: fid) (b: block) : Prop :=
    exists n, get_block (get_fl x f) n = b.
  
  Theorem freelist_norepeat:
    forall x f, wd x -> norep (flist_content x f).
  
  Theorem freelist_disjoint:
    forall x f1 f2, wd x -> f1 <> f2 -> disj (flist_content x f1) (flist_content x f2).
  
  Theorem thread_freelist_norepeat:
    forall x i nf, wd x -> norep (get_tfl x i nf).

  Theorem thread_freelist_disj:
    forall x i1 i2 nf1 nf2, wd x -> i1 <> i2 -> disj (get_tfl x i1 nf1) (get_tfl x i2 nf2).

End FLists.
        

The global environment for all modules

Module GlobEnv.

  Record t: Type :=
    {
      M: nat;
      modules: 'I_M -> ModSem.t;
      get_mod: ident -> option 'I_M;
      ge_bound: block;
      freelists: FLists.t;
    }.

  Record wd (GE: t) : Prop :=
    {
      wd_fl: FLists.wd GE.(freelists)
      ;
      ge_inj: forall (i1 i2: 'I_(M GE)) Mod1 Mod2 id1 id2 b,
          ~ Nat.eq i1 i2 ->
          (modules GE) i1 = Mod1 ->
          (modules GE) i2 = Mod2 ->
          let: ge1 := ModSem.ge Mod1 in
          let: ge2 := ModSem.ge Mod2 in
          Genv.find_symbol ge1 id1 = Some b ->
          Genv.find_symbol ge2 id2 = Some b ->
          id1 = id2
      ;
      ge_consist: forall (i1 i2: 'I_(M GE)) Mod1 Mod2 id b1 b2,
          (modules GE) i1 = Mod1 ->
          (modules GE) i2 = Mod2 ->
          let: ge1 := ModSem.ge Mod1 in
          let: ge2 := ModSem.ge Mod2 in
          Genv.find_symbol ge1 id = Some b1 ->
          Genv.find_symbol ge2 id = Some b2 ->
          b1 = b2
      ;
      ge_bound_consist:
        forall i Mod, modules GE i = Mod ->
                 let: ge := ModSem.ge Mod in
                 Genv.genv_next ge = ge_bound GE;
             
    }.

  Definition det (GE: t) : Prop :=
    forall ix, mod_det (modules GE ix).

  Definition mods_wd (GE: t) : Prop :=
    forall ix, mod_wd (modules GE ix).
  
  Record init {NL: nat} {L: @langs NL} (cus: cunits L) (GE: t): Prop :=
    {
      mod_num: (M GE) = length cus
      ;
      ge_init: forall (i: 'I_(M GE)),
          (exists cui, nth_error cus i = Some cui /\
                       let: Mod:= (modules GE) i in
                       ModSem.init_modsem (L (lid L cui)) (cu L cui) Mod)
      ;
      get_mod_init:
        forall id mid,
          (get_mod GE id) = Some mid <->
          snd (@fold_left (nat * (option nat)) (cunit L)
                          (fun ir cui => let (i, res) := ir in
                                      if res then (S i, res)
                                      else if In_dec peq id (internal_fn (L (lid L cui)) (cu L cui))
                                           then (S i, Some i)
                                           else (S i, res))
                          cus (0%nat, None))
          = Some (nat_of_ord mid)
      ;
      
      ge_wd: wd GE;
          
    }.

  Inductive init_mem: t -> gmem -> Prop :=
  | Init_mem : forall GE gm,
      (forall i,
          let: Mod := modules GE i in
          let: l := ModSem.lang Mod in
          let: ge := ModSem.ge Mod in
          init_gmem l ge gm) ->
      (forall fi,
          no_overlap (FLists.get_fl (freelists GE) fi) (valid_block_bset gm)) ->
      init_mem GE gm.

End GlobEnv.

Core.t

Module Core.
  Section Core.
    Context {ge: GlobEnv.t}.
    
    Record t : Type :=
      {
        i : 'I_ge.(GlobEnv.M);

        c : (ge.(GlobEnv.modules) i).(ModSem.lang).(core);
        sg : signature;
        
        F : fid;
      }.

    Inductive update
              (x: t)
              (c': (ge.(GlobEnv.modules) x.(i)).(ModSem.lang).(core))
      : t -> Prop :=
      Update: forall x',
        x' = Build_t x.(i) c' x.(sg) x.(F) -> update x c' x'.

  End Core.
End Core.

CallStack.t

Module CallStack.
  Section CallStack.
    Context {ge: GlobEnv.t}.

    Definition t : Type := list (@Core.t ge).

    Definition emp_cs : t := nil.
    Definition push (c: Core.t) (cs: t) : t := c :: cs.
    Definition pop (cs: t) : option t :=
      match cs with
      | nil => None
      | c :: cs' => Some cs'
      end.
    Definition top (cs: t) : option Core.t :=
      match cs with
      | nil => None
      | c :: cs' => Some c
      end.
    Inductive update : t -> Core.t -> t -> Prop :=
      Update : forall c cs cc c',
        Core.update c cc c' ->
        update (c::cs) c' (c'::cs).

    Definition is_emp (cs: t) : Prop := cs = nil.
    
  End CallStack.
End CallStack.

ThreadPool.t

Module ThreadPool.
  Section ThreadPool.
    Context {ge: GlobEnv.t}.

    Record t : Type :=
      {
        content: PMap.t (option (@CallStack.t ge));
        next_tid: tid;
        next_fmap: tid -> nat;
      }.

    Definition emp: t := Build_t (PMap.init None) 1%positive (fun _ => 0%nat).
      
    Definition spawn (thdp: t)
               (mid: 'I_(GlobEnv.M ge))
               (c: core (ModSem.lang (GlobEnv.modules ge mid)))
               (sg: signature) : t :=
      let: nf := (thdp.(next_fmap) thdp.(next_tid)) in
      let: f := FLists.get_tfid (GlobEnv.freelists ge) (thdp.(next_tid)) nf in
      let: c := Core.Build_t mid c sg f in
      Build_t (PMap.set thdp.(next_tid) (Some (c::nil)) thdp.(content))
              (Psucc thdp.(next_tid))
              (fun i => if peq i thdp.(next_tid) then (S (thdp.(next_fmap) i))
                        else thdp.(next_fmap) i).

    Definition push (thdp: t) (i: tid)
               (mid: 'I_(GlobEnv.M ge))
               (c: core (ModSem.lang (GlobEnv.modules ge mid)))
               (sg: signature) : option t :=
      let: ocs := PMap.get i thdp.(content) in
      match ocs with
      | None => None
      | Some cs =>
        let: nf := (thdp.(next_fmap) i) in
        let: f := FLists.get_tfid (GlobEnv.freelists ge) i nf in
        let: c := Core.Build_t mid c sg f in
        Some
          (Build_t (PMap.set i (Some (CallStack.push c cs)) thdp.(content))
                   (thdp.(next_tid))
                   (fun i' => if peq i i' then (S (thdp.(next_fmap) i))
                             else thdp.(next_fmap) i')
          )
      end.


        
    Definition pop (thdp: t) (i: tid) : option t :=
      let: ocs := PMap.get i thdp.(content) in
      match ocs with
      | None => None
      | Some cs =>
        match CallStack.pop cs with
        | None => None
        | Some cs' =>
          Some (Build_t (PMap.set i (Some cs') thdp.(content))
                        (thdp.(next_tid)) (thdp.(next_fmap)))
        end
      end.

    Definition get_cs (thdp: t) (i: tid) : option CallStack.t :=
      PMap.get i thdp.(content).
    
    Definition get_top (thdp: t) (i: tid) : option Core.t :=
      match get_cs thdp i with
      | Some cs => CallStack.top cs
      | None => None
      end.

    Inductive update (thdp: t) (i: tid) (c: Core.t) : t -> Prop :=
      Update : forall cs cs' thdp',
        get_cs thdp i = Some cs ->
        CallStack.update cs c cs' ->
        thdp' = Build_t (PMap.set i (Some cs') thdp.(content))
                        (thdp.(next_tid)) (thdp.(next_fmap)) ->
        update thdp i c thdp'.

    
    Inductive init : entries -> t -> Prop :=
    | init_nil : init nil emp
    | init_cons :
        forall funid m_id,
          GlobEnv.get_mod ge funid = Some m_id ->
          forall e thdp cc,
            init e thdp ->
            let: Mod := GlobEnv.modules ge m_id in
            let: l := ModSem.lang Mod in
            let: Ge := ModSem.Ge Mod in
            l.(init_core) Ge funid nil = Some cc ->
            let: thdp':= spawn thdp m_id cc signature_main in
            init (funid :: e) thdp'.
        
    Definition valid_tid (TP:t) (i:tid) := Plt i (next_tid TP).

    Inductive halted : t -> tid -> Prop :=
    | Halted : forall TP i cs,
        get_cs TP i = Some cs -> CallStack.is_emp cs ->
        halted TP i.
                          
    Record inv_cs (cs: CallStack.t) (i: tid) (next: nat) : Prop :=
      {
        fid_belongsto: forall c,
            In c cs ->
            FLists.fbelongsto (ge.(GlobEnv.freelists)) i c.(Core.F);
        fid_valid: forall c,
            In c cs ->
            exists n, (n < next)%nat /\
                      FLists.get_tfid (ge.(GlobEnv.freelists)) i n = c.(Core.F);
        fid_disjoint:
          forall n1 n2 (core1 core2: @Core.t ge),
            nth_error cs n1 = Some core1 ->
            nth_error cs n2 = Some core2 ->
            (Core.F core1) = (Core.F core2) ->
            n1 = n2;
      }.

    Lemma cs_upd_inv_cs:
      forall (cs: @CallStack.t ge) c cs' i f,
        inv_cs cs i f ->
        CallStack.update cs c cs' ->
        inv_cs cs' i f.

    Lemma cs_push_inv_cs:
      forall cs ix cc sg cs' i nf,
        GlobEnv.wd ge ->
        inv_cs cs i nf ->
        CallStack.push
          {|Core.i := ix; Core.c := cc; Core.sg := sg;
            Core.F := FLists.get_tfid (GlobEnv.freelists ge) i nf |} cs
        = cs' ->
        inv_cs cs' i (S nf).

    Lemma cs_pop_inv_cs:
      forall cs cs' i nf,
        inv_cs cs i nf ->
        CallStack.pop cs = Some cs' ->
        inv_cs cs' i nf.
      
    Record inv (thdp: t) : Prop :=
      {
        tp_finite: forall i,
            Pge i thdp.(next_tid) -> PMap.get i thdp.(content) = None;
        tp_valid: forall i,
            Plt i thdp.(next_tid) -> exists cs, PMap.get i thdp.(content) = Some cs;
        thdp_default: fst thdp.(content) = None;
        cs_inv: forall i cs,
          PMap.get i thdp.(content) = Some cs ->
          inv_cs cs i (thdp.(next_fmap) i);
      }.

    Lemma emp_inv: inv emp.

    Lemma spawn_inv:
      forall tp mid c sg tp',
        spawn tp mid c sg = tp' ->
        inv tp ->
        inv tp'.

    Lemma init_inv:
      forall el tp,
        init el tp ->
        inv tp.
      
    Lemma upd_top_inv:
      forall tp i c cc c' tp',
        inv tp ->
        get_top tp i = Some c ->
        Core.update c cc c' ->
        update tp i c' tp' ->
        inv tp'.

    Lemma push_inv:
      forall tp i ix cc sg tp',
        GlobEnv.wd ge ->
        inv tp ->
        push tp i ix cc sg = Some tp' ->
        inv tp'.

    Lemma pop_inv:
      forall tp i tp',
        inv tp ->
        pop tp i = Some tp' ->
        inv tp'.

    Record inv_mem (thdp: t) (gm: gmem) : Prop :=
      {
        tp_valid_freelist_free:
          forall i n,
            (n >= (next_fmap thdp) i)%nat ->
            no_overlap (FLists.get_tfl (GlobEnv.freelists ge) i n) (valid_block_bset gm);
      }.
            
    Lemma push_top_fid:
      forall thdp i mid c sg thdp' C,
        push thdp i mid c sg = Some thdp' ->
        get_top thdp' i = Some C ->
        let nf := (thdp.(next_fmap) i) in
        let f := FLists.get_tfid (GlobEnv.freelists ge) i nf in
        Core.F C = f.
    
  End ThreadPool.
End ThreadPool.

Atomic bit

Inductive Bit : Type :=
| O : Bit
| I : Bit.

Runtime state

Record ProgConfig {GE: GlobEnv.t}: Type :=
  {
    thread_pool : @ThreadPool.t GE;
    cur_tid : tid;
    gm : gmem;
    atom_bit : Bit;
  }.

Initial state

Inductive init_config
          {NL: nat} {L: @langs NL} (p: @prog NL L)
          (m:gmem) (GE: GlobEnv.t) (pc: @ProgConfig GE) (t: tid): Prop :=
  Init_config:
    GlobEnv.init (fst p) GE ->
    GlobEnv.init_mem GE m ->
    ThreadPool.init (snd p) (pc.(thread_pool)) ->
    FLists.wd (GlobEnv.freelists GE) ->
    (forall fi, no_overlap (FLists.get_fl (GlobEnv.freelists GE) fi) (valid_block_bset m)) ->
    reach_closed m (valid_block_bset m) ->
    cur_tid pc = t ->
    Plt t (ThreadPool.next_tid pc.(thread_pool)) ->
    (atom_bit pc) = O ->
    (gm pc) = m ->
    init_config p m GE pc t.

Lemma init_config_GE_wd:
  forall NL L (p:@prog NL L) gm GE pc t,
    init_config p gm GE pc t ->
    GlobEnv.wd GE.

Final state

Inductive final_state {ge: GlobEnv.t} : @ProgConfig ge -> Prop :=
| Final_state : forall pc TP,
    thread_pool pc = TP ->
    (forall i, ThreadPool.valid_tid TP i -> ThreadPool.halted TP i) ->
    final_state pc.

Realtion on initial memories

Record InitRel (mu: Mu) (SGE TGE: GlobEnv.t) (sgm tgm: gmem) : Prop :=
  {
    ir_inject: GMem.Binject_weak (inj mu) sgm tgm;
    ir_mu_wd: Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu);
    ir_shared_src: SharedSrc mu = fun b => Plt b (GlobEnv.ge_bound SGE);
    ir_shared_tgt: SharedTgt mu = fun b => Plt b (GlobEnv.ge_bound TGE);
    ir_ge_bound: GlobEnv.ge_bound SGE = GlobEnv.ge_bound TGE;
    
    ir_senv_init_inj:
      forall (m: 'I_(GlobEnv.M SGE)) (n: 'I_(GlobEnv.M TGE)),
        nat_of_ord m = nat_of_ord n ->
        let Modm := GlobEnv.modules SGE m in
        let Modn := GlobEnv.modules TGE n in
        let sge := ModSem.ge Modm in
        let tge := ModSem.ge Modn in
        (forall id, option_rel (fun b b' => inj mu b = Some b')
                          (Senv.find_symbol sge id) (Senv.find_symbol tge id));
    
    ir_shared_src_valid: forall b, GMem.valid_block sgm b <-> Injections.SharedSrc mu b;
    ir_shared_tgt_valid: forall b, GMem.valid_block tgm b <-> Injections.SharedTgt mu b;
    
  }.


Definition res_has_type (res: val) (sg: signature) : Prop :=
  Val.has_type res (proj_sig_res sg).

Definition res_sg (sg: signature) (res: val) : option val :=
  match (sg.(sig_res)) with
  | None => None
  | Some _ => Some res
  end.

Definition not_pointer (v: val) : Prop :=
  match v with
  | Vptr _ _ => False
  | Vundef => False
  | _ => True
  end.