diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-03 18:36:10 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-03 18:36:16 +0100 |
| commit | c3b35b153f5f0023934e8d09007a68fd4a2a6b55 (patch) | |
| tree | ec0248109be75287dc764dfce787531b36525b80 /stm/asyncTaskQueue.ml | |
| parent | c4f270f573360e39bd91e3ffff8d37775b2871d7 (diff) | |
STM: code refactoring
This is mainly shuffling code around and removing internal
refs that are not needed anymore.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 22e7c0243..fa7aa9584 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -251,7 +251,7 @@ module Make(T : Task) = struct let slave_ic = ref stdin let slave_oc = ref stdout - let slave_init_stdout () = + let init_stdout () = let ic, oc = Spawned.get_channels () in slave_oc := oc; slave_ic := ic @@ -264,7 +264,7 @@ module Make(T : Task) = struct let slave_handshake () = WorkersPool.worker_handshake !slave_ic !slave_oc - let slave_main_loop reset = + let main_loop () = let feedback_queue = ref [] in let slave_feeder oc fb = match fb.Feedback.content with @@ -293,7 +293,7 @@ module Make(T : Task) = struct flush_feeder !slave_oc; report_status "Idle"; marshal_response !slave_oc response; - reset () + Ephemeron.clear () with | MarshalError s -> pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 @@ -328,3 +328,6 @@ module Make(T : Task) = struct let n_workers = WorkersPool.n_workers end + +module MakeQueue(T : Task) = struct include Make(T) end +module MakeWorker(T : Task) = struct include Make(T) end |