fworkshop.out

(***********************************************************************)
(*                                                                     *)
(*                       ATS/contrib/libats-hwxi                       *)
(*                                                                     *)
(***********************************************************************)
(*
** Copyright (C) 2017 Hongwei Xi, ATS Trustful Software, Inc.
**
** Permission is hereby granted, free of charge, to any person obtaining a
** copy of this software and associated documentation files (the "Software"),
** to deal in the Software without restriction, including without limitation
** the rights to use, copy, modify, merge, publish, distribute, sublicense,
** and/or sell copies of the Software, and to permit persons to whom the
** Software is furnished to do so, subject to the following stated conditions:
** 
** The above copyright notice and this permission notice shall be included in
** all copies or substantial portions of the Software.
** 
** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL
** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
** IN THE SOFTWARE.
*)
(* ****** ****** *)
(*
** HX-2017-02-07: Start it now!
*)
(* ****** ****** *)
(*
//
// HX-2017-02-11:
// It is supposed to be
// included rather than staloaded
//
#define
ATS_PACKNAME "ATSCNTRB.HX.fworkshop"
//
*)
(* ****** ****** *)
staload UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)
staload AT = "libats/SATS/athread.sats"

typedef tid = $AT.tid
typedef spin1 = $AT.spin1

(* ****** ****** *)
abstype fws$store_type() = ptr

typedef fws$store = fws$store_type

(* ****** ****** *)
absvtype fws$fwork_vtype() = ptr

vtypedef fws$fwork = fws$fwork_vtype

(* ****** ****** *)
extern
fun fws$store_capacity() : intGte(1)

extern
fun fws$store_insert(fws$store, fws$fwork) : void

extern
fun fws$store_takeout(store : fws$store) : fws$fwork

extern
fun fws$fwork_process(fws$fwork) : int

(* ****** ****** *)
abstype fworkshop_type() = ptr

typedef fworkshop = fworkshop_type

(* ****** ****** *)
vtypedef fworkshop_struct = @{ FWS_spin = spin1
                             , FWS_store = fws$store
                             , FWS_workerlst = List0_vt(tid)
                             }

(* ****** ****** *)
extern
fun fworkshop_create_exn() : fworkshop

extern
fun fws$store_create_exn() : fws$store

(* ****** ****** *)
extern
fun fworkshop_add_tid(fws : fworkshop, tid) : void

(* ****** ****** *)
extern
fun fworkshop_get_spin(fws : fworkshop) : spin1

(* ****** ****** *)
extern
fun fworkshop_get_store(fws : fworkshop) : fws$store

(* ****** ****** *)
extern
fun fworkshop_get_nworker(fws : fworkshop) : intGte(0)

(* ****** ****** *)
extern
fun fworkshop_insert_work(fws : fworkshop, fwork : fws$fwork) : void

extern
fun fworkshop_takeout_work(fws : fworkshop) : fws$fwork

extern
fun fworkshop_process_work(fws : fworkshop, fwork : fws$fwork) : int

(* ****** ****** *)
extern
fun fworkshop_add_worker(fws : fworkshop) : int

extern
fun fworkshop_add_nworker {n:nat} (fws : fworkshop, int(n)) : natLte(n)

(* ****** ****** *)
local
  assume fworkshop_type() = ref(fworkshop_struct)
in
  (* ****** ****** *)
  implement fworkshop_add_nworker {n} (fws, n) =
    loop(0, 0) where
    { fun loop { i : nat | i <= n } (i : int(i), res : natLte(i)) :
        natLte(n) =
        let
          
        in
          if i < n then
            let
              val err = fworkshop_add_worker{}(fws)
            in
              if err = 0 then
                loop(i + 1, res + 1)
              else
                res
            end
          else
            res
        end }
  
  (* ****** ****** *)
  implement fworkshop_add_worker (fws) =
    err where
    { fun fworker(fws : fworkshop) : void =
        let
          val fwork = fworkshop_takeout_work(fws)
          val status = fworkshop_process_work(fws, fwork)
        in
          if (status >= 0) then
            fworker(fws)
          else
            fworker_exit(fws)
        end
      
      and fworker_exit(fws : fworkshop) : void =
        let
          val tid0 = $AT.athread_self()
          
          fun auxrmv(tids : &List0_vt(tid) >> _) : void =
            (case+ tids of
              | list_vt_nil() => ()
              | @list_vt_cons (tid, tids_tl) => (if (tid0 != tid) then
                {
                  val () = auxrmv(tids_tl)
                  val () = fold@(tids)
                }
              else
                {
                  val tids_ = tids
                  val () = tids := tids_tl
                  val () = free@{..,0}(tids_)
                }))
          
          val (vbox pf | p0) = ref_get_viewptr(fws)
          val spn = p0->FWS_spin
          val (pflock | ()) = $AT.spin_lock(spn)
          val () = $effmask_ref(auxrmv(p0->FWS_workerlst))
          val () = $AT.spin_unlock(pflock | spn)
        in end
      
      var tid: lint? with 
      val err = $AT.athread_create_cloptr{}(tid, llam () => fworker(fws))
      val () = if (err = 0) then
        fworkshop_add_tid{}(fws, tid) }
  
  (* ****** ****** *)
  implement fworkshop_get_nworker (fws) =
    let
      val (vbox pf | p0) = ref_get_viewptr(fws)
      val spn = p0->FWS_spin
      val (pflock | ()) = $AT.spin_lock(spn)
      val nworker = list_vt_length(p0->FWS_workerlst)
      val () = $AT.spin_unlock(pflock | spn)
    in
      nworker
    end
  
  (* ****** ****** *)
  implement fworkshop_get_store (fws) =
    let
      val (vbox pf | p0) = ref_get_viewptr(fws)
    in
      p0->FWS_store
    end
  
  (* ****** ****** *)
  implement fworkshop_get_spin (fws) =
    let
      val (vbox pf | p0) = ref_get_viewptr(fws)
    in
      p0->FWS_spin
    end
  
  (* ****** ****** *)
  implement fworkshop_add_tid (fws, tid) =
    let
      val (vbox pf | p0) = ref_get_viewptr(fws)
      val spn = p0->FWS_spin
      val (pflock | ()) = $AT.spin_lock(spn)
      val tids = p0->FWS_workerlst
      val () = p0->FWS_workerlst := list_vt_cons(tid, tids)
      val () = $AT.spin_unlock(pflock | spn)
    in end
  
  (* ****** ****** *)
  implement fworkshop_create_exn () =
    let
      val (pf, fpf | p0) = ptr_alloc<fworkshop_struct>()
      val () = p0->FWS_spin := $AT.spin_create_exn()
      val () = p0->FWS_store := fws$store_create_exn{}(())
      val () = p0->FWS_workerlst := list_vt_nil()
    in
      $UN.castvwtp0{fworkshop}((p0, fpf, pf))
    end
  
  (* ****** ****** *)
end

(* ****** ****** *)
implement fworkshop_insert_work (fws, x0) =
  let
    val store = fworkshop_get_store{}(fws)
  in
    fws$store_insert{}(store, x0)
  end

(* ****** ****** *)
implement fworkshop_takeout_work (fws) =
  let
    val store = fworkshop_get_store{}(fws)
  in
    fws$store_takeout{}(store)
  end

(* ****** ****** *)
implement fworkshop_process_work (fws, fwork) =
  status where
  { val status = fws$fwork_process{}(fwork) }

(* ****** ****** *)
(* end of [fworkshop.dats] *)