Skip to content

Commit 7220d3a

Browse files
bartoszmodelskibartoszmodelski
committed
.
1 parent 337fc79 commit 7220d3a

File tree

1 file changed

+129
-129
lines changed

1 file changed

+129
-129
lines changed

‎src/tracedAtomic.ml‎

Lines changed: 129 additions & 129 deletions
Original file line numberDiff line numberDiff line change
@@ -296,19 +296,18 @@ let rec explore_source depth func state sleep_sets =
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 -> ()
300-
(* Printf.printf "[depth=%d] rtn\n%!" depth *)
299+
| None -> () (* Printf.printf "[depth=%d] rtn\n%!" depth *)
301300
| Some p ->
302301
s.backtrack <- IntSet.singleton p;
303302

304303
while IntSet.(cardinal (diff s.backtrack !sleep)) > 0 do
305304
(* Printf.printf "[depth=%d] loop (backtrack=[%s], sleep=[%s])\n%!" depth
306-
(_set_to_str s.backtrack) (_set_to_str !sleep); *)
305+
(_set_to_str s.backtrack) (_set_to_str !sleep); *)
307306
let p = IntSet.min_elt (IntSet.diff s.backtrack !sleep) in
308307
let proc = List.nth s.procs p in
309308

310309
(* Printf.printf "[depth=%d] p=%d, %s, %s\n%!" depth p
311-
(atomic_op_str proc.op) (var_name proc.obj_ptr); *)
310+
(atomic_op_str proc.op) (var_name proc.obj_ptr); *)
312311
(* run *)
313312
let state_top =
314313
let schedule =
@@ -331,137 +330,137 @@ let rec explore_source depth func state sleep_sets =
331330
new_state
332331
in
333332

334-
let reversible_races =
335-
match reversible_races with
336-
| [] -> []
337-
| _ -> [ last_element reversible_races ]
333+
let most_recent_race =
334+
match List.rev reversible_races with [] -> None | v :: _ -> Some v
338335
in
339336

340337
(* Printf.printf "[depth=%d] reversible races sz: %d\n%!" depth
341338
(List.length reversible_races); *)
342-
for i = 0 to List.length reversible_races - 1 do
343-
let e = List.nth reversible_races i in
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); *)
347-
let found_e, prefix_rev, suffix_rev =
348-
List.fold_left
349-
(fun (seen_e, prefix, suffix) proc' ->
350-
if seen_e then (seen_e, prefix, proc' :: suffix)
351-
else if proc' == e then (true, prefix, suffix)
352-
else (false, proc' :: prefix, suffix))
353-
(false, [], []) state
354-
in
355-
assert (
356-
List.length prefix_rev + List.length suffix_rev
357-
= List.length state - 1);
358-
assert found_e;
359-
360-
if List.length prefix_rev > 0 then (
361-
let prefix (* E' *) = List.rev prefix_rev in
362-
(* List.iter
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; *)
369-
let suffix = List.rev suffix_rev in
370-
371-
(* List.iter
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; *)
378-
let prefix_top = last_element prefix in
379-
339+
(match most_recent_race with
340+
| None -> ()
341+
| Some e ->
380342
(* Printf.printf
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); *)
384-
let v_E (* occurs after e but independent of e *) =
385-
List.filter
386-
(fun proc' ->
387-
proc'.run_proc <> e.run_proc
388-
&& Option.value proc'.run_ptr ~default:(-1)
389-
<> Option.value e.run_ptr ~default:(-2))
390-
suffix
343+
"[depth=%d] inner loop, racing op: e=(p'=%d, %s, %s)\n%!" depth
344+
e.run_proc (atomic_op_str e.run_op) (var_name e.run_ptr); *)
345+
let found_e, prefix_rev, suffix_rev =
346+
List.fold_left
347+
(fun (seen_e, prefix, suffix) proc' ->
348+
if seen_e then (seen_e, prefix, proc' :: suffix)
349+
else if proc' == e then (true, prefix, suffix)
350+
else (false, proc' :: prefix, suffix))
351+
(false, [], []) state
391352
in
353+
assert (
354+
List.length prefix_rev + List.length suffix_rev
355+
= List.length state - 1);
356+
assert found_e;
357+
358+
if List.length prefix_rev > 0 then
359+
let prefix (* E' *) = List.rev prefix_rev in
360+
(* List.iter
361+
(fun proc ->
362+
Printf.printf "[depth=%d] ::prefix:: (p=%d, %s, %s)\n%!"
363+
depth proc.run_proc
364+
(atomic_op_str proc.run_op)
365+
(var_name proc.run_ptr))
366+
prefix; *)
367+
let suffix = List.rev suffix_rev in
368+
369+
(* List.iter
370+
(fun proc ->
371+
Printf.printf "[depth=%d] ::suffix:: (p=%d, %s, %s)\n%!"
372+
depth proc.run_proc
373+
(atomic_op_str proc.run_op)
374+
(var_name proc.run_ptr))
375+
suffix; *)
376+
let prefix_top = last_element prefix in
377+
378+
(* Printf.printf
379+
"[depth=%d] nonempty prefix, prefix_top: (p=%d, %s)\n%!" depth
380+
prefix_top.run_proc
381+
(atomic_op_str prefix_top.run_op); *)
382+
let v_E (* occurs after e but independent of e *) =
383+
List.filter
384+
(fun proc' ->
385+
proc'.run_proc <> e.run_proc
386+
&& Option.value proc'.run_ptr ~default:(-1)
387+
<> Option.value e.run_ptr ~default:(-2))
388+
suffix
389+
in
392390

393-
(* List.iter
394-
(fun proc ->
395-
Printf.printf
396-
"[depth=%d] ::occurs_after_e_but_indep:: (p=%d, %s)\n%!"
397-
depth proc.run_proc
398-
(atomic_op_str proc.run_op))
399-
v_E; *)
400-
let v = v_E @ [ state_top ] in
401-
402-
(* List.iter
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; *)
408-
let initials =
409-
let initials_map, initials_spawns =
410-
List.fold_left
411-
(fun (first_accesses, spawns) (state_cell : state_cell) ->
412-
match state_cell.run_ptr with
413-
| None ->
414-
let new_spawns =
415-
IntSet.add state_cell.run_proc spawns
416-
in
417-
(first_accesses, new_spawns)
418-
| Some obj_ptr ->
419-
let new_first_accesses =
420-
IntMap.update obj_ptr
421-
(function
422-
| Some v -> Some v
423-
| None -> Some (`Run_proc state_cell.run_proc))
424-
first_accesses
425-
in
426-
(new_first_accesses, spawns))
427-
(IntMap.empty, IntSet.empty)
428-
v
391+
(* List.iter
392+
(fun proc ->
393+
Printf.printf
394+
"[depth=%d] ::occurs_after_e_but_indep:: (p=%d, %s)\n%!"
395+
depth proc.run_proc
396+
(atomic_op_str proc.run_op))
397+
v_E; *)
398+
let v = v_E @ [ state_top ] in
399+
400+
(* List.iter
401+
(fun proc ->
402+
Printf.printf "[depth=%d] ::v:: (p=%d, %s)\n%!" depth
403+
proc.run_proc
404+
(atomic_op_str proc.run_op))
405+
v; *)
406+
let initials =
407+
let initials_map, initials_spawns =
408+
List.fold_left
409+
(fun (first_accesses, spawns) (state_cell : state_cell) ->
410+
match state_cell.run_ptr with
411+
| None ->
412+
let new_spawns =
413+
IntSet.add state_cell.run_proc spawns
414+
in
415+
(first_accesses, new_spawns)
416+
| Some obj_ptr ->
417+
let new_first_accesses =
418+
IntMap.update obj_ptr
419+
(function
420+
| Some v -> Some v
421+
| None -> Some (`Run_proc state_cell.run_proc))
422+
first_accesses
423+
in
424+
(new_first_accesses, spawns))
425+
(IntMap.empty, IntSet.empty)
426+
v
427+
in
428+
IntMap.fold
429+
(fun _obj_ptr (`Run_proc run_proc) initials_set ->
430+
IntSet.add run_proc initials_set)
431+
initials_map initials_spawns
429432
in
430-
IntMap.fold
431-
(fun _obj_ptr (`Run_proc run_proc) initials_set ->
432-
IntSet.add run_proc initials_set)
433-
initials_map initials_spawns
434-
in
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
433+
(*
434+
Printf.printf
435+
"[depth=%d] initials=[%s], backtrack=[%s] at depth=%d, p=%d, \
436+
op=%s \n\
437+
%!"
438+
depth (_set_to_str initials)
439+
(_set_to_str prefix_top.backtrack)
440+
(List.length prefix - 1)
441+
prefix_top.run_proc
442+
(atomic_op_str prefix_top.run_op); *)
443+
let prefix_top_sleep =
444+
!(List.nth sleep_sets (List.length prefix - 1))
458445
in
459-
(*
460-
Printf.printf "[depth=%d] adding initial to backtrack\n%!"
461-
depth; *)
462-
prefix_top.backtrack <- IntSet.add _initial prefix_top.backtrack))
463-
done;
464-
446+
if
447+
IntSet.(
448+
cardinal
449+
(inter prefix_top.backtrack
450+
(diff initials prefix_top_sleep)))
451+
= 0
452+
then
453+
let initial =
454+
match
455+
IntSet.(min_elt_opt (diff initials prefix_top_sleep))
456+
with
457+
| Some initial -> initial
458+
| None -> IntSet.min_elt initials
459+
in
460+
(*
461+
Printf.printf "[depth=%d] adding initial to backtrack\n%!"
462+
depth; *)
463+
prefix_top.backtrack <- IntSet.add initial prefix_top.backtrack);
465464
let sleep' =
466465
IntSet.filter
467466
(fun q ->
@@ -476,9 +475,10 @@ let rec explore_source depth func state sleep_sets =
476475
in
477476
explore_source (depth + 1) func new_state (sleep_sets @ [ ref sleep' ]);
478477
sleep := IntSet.add p !sleep
479-
done;;
480-
(* Printf.printf "[depth=%d] exit (backtrack=[%s], sleep=[%s])\n%!" depth
481-
(_set_to_str s.backtrack) (_set_to_str !sleep) *)
478+
done
479+
480+
(* Printf.printf "[depth=%d] exit (backtrack=[%s], sleep=[%s])\n%!" depth
481+
(_set_to_str s.backtrack) (_set_to_str !sleep) *)
482482

483483
let rec explore func state clock last_access =
484484
let s = last_element state in

0 commit comments

Comments
 (0)