add program generation

Author: bartoszmodelski

dscheck.opam

@@ -13,6 +13,7 @@ depends: [
   "tsort"
   "oseq"
   "alcotest" {>= "1.6.0" & with-test}
+  "cmdliner"
   "odoc" {with-doc}
 ]
 build: [

dune-project

@@ -11,6 +11,6 @@
 (package
  (name dscheck)
  (synopsis "Traced Atomics")
- (depends (ocaml (>= 5.0.0)) dune containers tsort oseq (alcotest (and (>= 1.6.0) :with-test))))
+ (depends (ocaml (>= 5.0.0)) dune containers tsort oseq (alcotest (and (>= 1.6.0) :with-test)) cmdliner))
 
 

src/trace_tracker.ml

@@ -101,3 +101,6 @@ let equal t1 t2 =
       (* any values under the same key are known to be equivalent, even if the exact sequence is not identical *))
     t1 t2
   == 0
+
+let subset t1 t2 =
+  TraceMap.fold (fun key _ seen_all -> TraceMap.mem key t2 && seen_all) t1 true

src/trace_tracker.mli

@@ -7,3 +7,4 @@ val print_traces : out_channel -> unit
 val print : t -> out_channel -> unit
 val equal : t -> t -> bool
 val get_deps_str : t -> string
+val subset : t -> t -> bool

src/tracedAtomic.ml

@@ -310,6 +310,22 @@ let do_run init_func init_schedule =
         backtrack = IntSet.empty;
       }
 
+let rec explore_random func state =
+  let s = last_element state in
+  let enabled = IntSet.to_seq s.enabled |> List.of_seq in
+  let len = List.length enabled in
+  if len == 0 then ()
+  else
+    let random_index = Random.int len in
+    let j = List.nth enabled random_index in
+    let j_proc = List.nth s.procs j in
+    let schedule =
+      List.map (fun s -> (s.run_proc, s.run_op, s.run_ptr)) state
+      @ [ (j, j_proc.op, j_proc.obj_ptr) ]
+    in
+    let statedash = state @ [ do_run func schedule ] in
+    explore_random func statedash
+
 let rec explore func state clock last_access =
   let s = last_element state in
   List.iter
@@ -371,18 +387,25 @@ let reset_state () =
 
 let dscheck_trace_file_env = Sys.getenv_opt "dscheck_trace_file"
 
+let random func iters =
+  reset_state ();
+  let empty_state = do_run func [ (0, Start, None) ] :: [] in
+  for _ = 1 to iters do
+    explore_random func empty_state
+  done
+
 let dpor func =
   reset_state ();
   let empty_state = do_run func [ (0, Start, None) ] :: [] in
   let empty_clock = IntMap.empty in
   let empty_last_access = IntMap.empty in
   explore func empty_state empty_clock empty_last_access
 
-let trace ?interleavings ?(record_traces = false) func =
+let trace ?(impl = `Dpor) ?interleavings ?(record_traces = false) func =
   record_traces_flag := record_traces || Option.is_some dscheck_trace_file_env;
   interleavings_chan := interleavings;
 
-  dpor func;
+  (match impl with `Dpor -> dpor func | `Random iters -> random func iters);
 
   (* print reports *)
   (match !interleavings_chan with

src/tracedAtomic.mli

@@ -47,9 +47,15 @@ val decr : int t -> unit
 (** [decr r] atomically decrements the value of [r] by [1]. *)
 
 val trace :
-  ?interleavings:out_channel -> ?record_traces:bool -> (unit -> unit) -> unit
+  ?impl:[ `Random of int | `Dpor ] ->
+  ?interleavings:out_channel ->
+  ?record_traces:bool ->
+  (unit -> unit) ->
+  unit
 (** [trace ?interleavings ?record_traces f] starts the simulation trace.
 
+  [impl] lets user choose the underlying exploration algorithm.
+
   If [interleavings] output channel is provided, DSCheck will continously
   print the visited interleavings there.
 

tests/dune

@@ -37,3 +37,8 @@
  (name test_conditional_ssb)
  (libraries dscheck alcotest)
  (modules test_conditional_ssb))
+
+(executable
+ (name gen_program)
+ (libraries dscheck cmdliner)
+ (modules gen_program))