Skip to content

Commit 858271f

Browse files
bartoszmodelskibartoszmodelski
committed
possible fix
.
1 parent 813a8cb commit 858271f

File tree

2 files changed

+85
-56
lines changed

2 files changed

+85
-56
lines changed

‎src/tracedAtomic.ml‎

Lines changed: 84 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -198,26 +198,26 @@ let num_traces = ref 0
198198
(* we stash the current state in case a check fails and we need to log it *)
199199
let schedule_for_checks = ref []
200200

201+
let var_name i =
202+
match i with
203+
| None -> ""
204+
| Some i ->
205+
let c = Char.chr (i + 97) in
206+
let seq = Seq.cons c Seq.empty in
207+
String.of_seq seq
208+
201209
let print_trace () =
202210
Printf.printf "-----------------------\n";
203-
List.iter
204-
(fun s ->
211+
List.iteri
212+
(fun i s ->
205213
match s with
206214
| last_run_proc, last_run_op, last_run_ptr ->
207-
let var_name i =
208-
let c = Char.chr (i + 97) in
209-
let seq = Seq.cons c Seq.empty in
210-
String.of_seq seq
211-
in
215+
let last_run_ptr = var_name last_run_ptr in
212216

213-
let last_run_ptr =
214-
Option.map (* string_of_int *) var_name last_run_ptr
215-
|> Option.value ~default:""
216-
in
217217
let tabs =
218218
List.init last_run_proc (fun _ -> "\t\t") |> String.concat ""
219219
in
220-
Printf.printf "%sP%d: %s %s\n" tabs last_run_proc
220+
Printf.printf "[depth=%d] %sP%d: %s %s\n" i tabs last_run_proc
221221
(atomic_op_str last_run_op)
222222
last_run_ptr)
223223
!schedule_for_checks;
@@ -239,7 +239,7 @@ let do_run init_func init_schedule =
239239
| [] ->
240240
if !finished_processes == num_processes then (
241241
tracing := false;
242-
print_trace ();
242+
(* print_trace (); *)
243243
num_traces := !num_traces + 1;
244244
!final_func ();
245245
tracing := true)
@@ -289,24 +289,26 @@ let do_run init_func init_schedule =
289289
let _set_to_str s =
290290
IntSet.to_seq s |> List.of_seq |> List.map Int.to_string |> String.concat ", "
291291

292-
let rec explore_source depth func state sleep =
293-
(* sleep := IntSet.empty; *)
292+
let rec explore_source depth func state sleep_sets =
293+
let sleep = last_element sleep_sets in
294294
let s = last_element state in
295295
(* Printf.printf "[depth=%d] explore (backtrack=[%s], sleep=[%s], enabled=[%s])\n%!" depth
296296
(set_to_str s.backtrack) (set_to_str !sleep) (set_to_str s.enabled); *)
297297
let p_maybe = IntSet.min_elt_opt (IntSet.diff s.enabled !sleep) in
298298
match p_maybe with
299-
| None -> () (* Printf.printf "[depth=%d] rtn\n%!" depth *)
299+
| None -> ()
300+
(* Printf.printf "[depth=%d] rtn\n%!" depth *)
300301
| Some p ->
301302
s.backtrack <- IntSet.singleton p;
302303

303304
while IntSet.(cardinal (diff s.backtrack !sleep)) > 0 do
304305
(* Printf.printf "[depth=%d] loop (backtrack=[%s], sleep=[%s])\n%!" depth
305-
(set_to_str s.backtrack) (set_to_str !sleep); *)
306+
(_set_to_str s.backtrack) (_set_to_str !sleep); *)
306307
let p = IntSet.min_elt (IntSet.diff s.backtrack !sleep) in
307308
let proc = List.nth s.procs p in
308309

309-
(* Printf.printf "[depth=%d] p=%d, %s\n%!" depth p (atomic_op_str proc.op); *)
310+
(* Printf.printf "[depth=%d] p=%d, %s, %s\n%!" depth p
311+
(atomic_op_str proc.op) (var_name proc.obj_ptr); *)
310312
(* run *)
311313
let state_top =
312314
let schedule =
@@ -323,10 +325,12 @@ let rec explore_source depth func state sleep =
323325
let reversible_races =
324326
List.filter
325327
(fun proc' ->
326-
let run_ptr = Option.value proc'.run_ptr ~default:(-2) in
327-
obj_ptr = run_ptr && proc'.run_proc <> p)
328+
match proc'.run_ptr with
329+
| None -> false
330+
| Some run_ptr -> obj_ptr = run_ptr && proc'.run_proc <> p)
328331
new_state
329332
in
333+
330334
let reversible_races =
331335
match reversible_races with
332336
| [] -> []
@@ -337,8 +341,9 @@ let rec explore_source depth func state sleep =
337341
(List.length reversible_races); *)
338342
for i = 0 to List.length reversible_races - 1 do
339343
let e = List.nth reversible_races i in
340-
(* Printf.printf "[depth=%d] inner loop, racing op: e=(q=%d, %s)\n%!"
341-
depth e.run_proc (atomic_op_str e.run_op); *)
344+
(* Printf.printf
345+
"[depth=%d] inner loop, racing op: e=(p'=%d, %s, %s)\n%!" depth
346+
e.run_proc (atomic_op_str e.run_op) (var_name e.run_ptr); *)
342347
let found_e, prefix_rev, suffix_rev =
343348
List.fold_left
344349
(fun (seen_e, prefix, suffix) proc' ->
@@ -351,29 +356,31 @@ let rec explore_source depth func state sleep =
351356
List.length prefix_rev + List.length suffix_rev
352357
= List.length state - 1);
353358
assert found_e;
354-
let prefix (* E' *) = List.rev prefix_rev in
355359

356-
if List.length prefix > 0 then
360+
if List.length prefix_rev > 0 then (
361+
let prefix (* E' *) = List.rev prefix_rev in
357362
(* List.iter
358-
(fun proc ->
359-
Printf.printf "[depth=%d] ::prefix:: (p=%d, %s)\n%!" depth
360-
proc.run_proc
361-
(atomic_op_str proc.run_op))
362-
prefix; *)
363+
(fun proc ->
364+
Printf.printf "[depth=%d] ::prefix:: (p=%d, %s, %s)\n%!"
365+
depth proc.run_proc
366+
(atomic_op_str proc.run_op)
367+
(var_name proc.run_ptr))
368+
prefix; *)
363369
let suffix = List.rev suffix_rev in
364370

365371
(* List.iter
366-
(fun proc ->
367-
Printf.printf "[depth=%d] ::suffix:: (p=%d, %s)\n%!" depth
368-
proc.run_proc
369-
(atomic_op_str proc.run_op))
370-
suffix; *)
372+
(fun proc ->
373+
Printf.printf "[depth=%d] ::suffix:: (p=%d, %s, %s)\n%!"
374+
depth proc.run_proc
375+
(atomic_op_str proc.run_op)
376+
(var_name proc.run_ptr))
377+
suffix; *)
371378
let prefix_top = last_element prefix in
372379

373380
(* Printf.printf
374-
"[depth=%d] nonempty prefix, prefix_top: (p=%d, %s)\n%!" depth
375-
prefix_top.run_proc
376-
(atomic_op_str prefix_top.run_op); *)
381+
"[depth=%d] nonempty prefix, prefix_top: (p=%d, %s)\n%!" depth
382+
prefix_top.run_proc
383+
(atomic_op_str prefix_top.run_op); *)
377384
let v_E (* occurs after e but independent of e *) =
378385
List.filter
379386
(fun proc' ->
@@ -393,11 +400,11 @@ let rec explore_source depth func state sleep =
393400
let v = v_E @ [ state_top ] in
394401

395402
(* List.iter
396-
(fun proc ->
397-
Printf.printf "[depth=%d] ::v:: (p=%d, %s)\n%!" depth
398-
proc.run_proc
399-
(atomic_op_str proc.run_op))
400-
v; *)
403+
(fun proc ->
404+
Printf.printf "[depth=%d] ::v:: (p=%d, %s)\n%!" depth
405+
proc.run_proc
406+
(atomic_op_str proc.run_op))
407+
v; *)
401408
let initials =
402409
let initials_map, initials_spawns =
403410
List.fold_left
@@ -413,27 +420,46 @@ let rec explore_source depth func state sleep =
413420
IntMap.update obj_ptr
414421
(function
415422
| Some v -> Some v
416-
| None -> Some state_cell.run_proc)
423+
| None -> Some (`Run_proc state_cell.run_proc))
417424
first_accesses
418425
in
419426
(new_first_accesses, spawns))
420427
(IntMap.empty, IntSet.empty)
421428
v
422429
in
423430
IntMap.fold
424-
(fun _ run_proc initials_set ->
431+
(fun _obj_ptr (`Run_proc run_proc) initials_set ->
425432
IntSet.add run_proc initials_set)
426433
initials_map initials_spawns
427434
in
428-
429-
(* Printf.printf "[depth=%d] initials=[%s], backtrack=[%s]\n%!"
430-
depth (set_to_str initials)
431-
(set_to_str prefix_top.backtrack); *)
432-
if IntSet.(cardinal (inter prefix_top.backtrack initials)) = 0 then
433-
let _initial = IntSet.min_elt initials in
434-
(* Printf.printf "[depth=%d] adding initial to backtrack\n%!"
435-
depth; *)
436-
prefix_top.backtrack <- IntSet.add _initial prefix_top.backtrack
435+
(*
436+
Printf.printf
437+
"[depth=%d] initials=[%s], backtrack=[%s] at depth=%d, p=%d, \
438+
op=%s \n\
439+
%!"
440+
depth (_set_to_str initials)
441+
(_set_to_str prefix_top.backtrack)
442+
(List.length prefix - 1)
443+
prefix_top.run_proc
444+
(atomic_op_str prefix_top.run_op); *)
445+
let prefix_top_sleep =
446+
!(List.nth sleep_sets (List.length prefix - 1))
447+
in
448+
if
449+
IntSet.(
450+
cardinal
451+
(inter prefix_top.backtrack (diff initials prefix_top_sleep)))
452+
= 0
453+
then (
454+
let _initial =
455+
match IntSet.(min_elt_opt (diff initials prefix_top_sleep)) with
456+
| Some initial -> initial
457+
| None -> IntSet.min_elt initials
458+
in
459+
(*
460+
Printf.printf "[depth=%d] adding initial to backtrack\n%!"
461+
depth; *)
462+
prefix_top.backtrack <- IntSet.add _initial prefix_top.backtrack))
437463
done;
438464

439465
let sleep' =
@@ -448,9 +474,11 @@ let rec explore_source depth func state sleep =
448474
| Some obj_ptr' -> obj_ptr' <> obj_ptr)
449475
!sleep
450476
in
451-
explore_source (depth + 1) func new_state (ref sleep');
477+
explore_source (depth + 1) func new_state (sleep_sets @ [ ref sleep' ]);
452478
sleep := IntSet.add p !sleep
453-
done
479+
done;;
480+
(* Printf.printf "[depth=%d] exit (backtrack=[%s], sleep=[%s])\n%!" depth
481+
(_set_to_str s.backtrack) (_set_to_str !sleep) *)
454482

455483
let rec explore func state clock last_access =
456484
let s = last_element state in
@@ -519,7 +547,7 @@ let _trace func =
519547
let _trace_source func =
520548
reset_state ();
521549
let empty_state = do_run func [ (0, Start, None) ] in
522-
explore_source 0 func [ empty_state ] (ref IntSet.empty)
550+
explore_source 1 func [ empty_state ] [ ref IntSet.empty ]
523551

524552
let trace func =
525553
_trace_source func;

‎tests/test_simple2.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,4 +16,5 @@ let test () =
1616
Format.printf "b=%i c=%i ok=%b@." (Atomic.get b) (Atomic.get c)
1717
(Atomic.get ok))
1818

19+
1920
let () = Atomic.trace test

0 commit comments

Comments
 (0)