Skip to content

Commit

Permalink
Document and rename API in wq.ml
Browse files Browse the repository at this point in the history
  • Loading branch information
krtab committed Aug 6, 2024
1 parent 22e4151 commit 40ca986
Show file tree
Hide file tree
Showing 4 changed files with 16 additions and 4 deletions.
2 changes: 1 addition & 1 deletion src/cmd/cmd_sym.ml
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
let pc = Choice.return (Ok ()) in
let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
let thread = Thread_with_memory.init () in
let res_queue = Wq.init () in
let res_queue = Wq.make () in
let callback v =
let open Symbolic_choice_intf in
match (fail_mode, v) with
Expand Down
2 changes: 1 addition & 1 deletion src/data_structures/wq.ml
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ let work_while f q = Synchronizer.work_while f q

let fail = Synchronizer.fail

let init () =
let make () =
let q = Queue.create () in
let writter v condvar =
let was_empty = Queue.is_empty q in
Expand Down
14 changes: 13 additions & 1 deletion src/data_structures/wq.mli
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,32 @@
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)

(** Synchronized FIFO queues *)

type !'a t

val init : unit -> 'a t
(** Create a new queue *)
val make : unit -> 'a t

(** Add a new element to the queue *)
val push : 'a -> 'a t -> unit

(** Get an element from the queue. The boolean shall be true to atomically start
a new pledge (cf make_pledge) while popping. *)
val pop : 'a t -> bool -> 'a option

(** Make a new pledge, ie indicate that new elements may be pushed to the queue
and that calls to pop should block waitting for them. *)
val make_pledge : 'a t -> unit

(** End one pledge. *)
val end_pledge : 'a t -> unit

(** Mark the queue as failed: all threads trying to pop from it will get no
element. *)
val fail : 'a t -> unit

(** Pop all elements from the queue in a lazy Seq.t, *)
val read_as_seq : 'a t -> finalizer:(unit -> unit) -> 'a Seq.t

val work_while : ('a -> ('a -> unit) -> unit) -> 'a t -> unit
2 changes: 1 addition & 1 deletion src/symbolic/symbolic_choice.ml
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ module CoreImpl = struct
type ('a, 'wls) t = { work_queue : ('a, 'wls) work_queue } [@@unboxed]

let init_scheduler () =
let work_queue = Wq.init () in
let work_queue = Wq.make () in
{ work_queue }

let add_init_task sched task = Wq.push task sched.work_queue
Expand Down

0 comments on commit 40ca986

Please sign in to comment.