From bdca42d8282e4a329982d3ff3f4a05cfbad90332 Mon Sep 17 00:00:00 2001 From: Arthur Carcano Date: Tue, 4 Jun 2024 15:18:50 +0200 Subject: [PATCH] Make Worker Local Storage actually local Before this fix, the "outter" wls was leaked through argumented_f to yielding tasks, which would then use the wrong WLS --- src/symbolic/symbolic_choice.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 9156d6c7a..08a852def 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -224,20 +224,22 @@ module Multicore = struct let return_status status = Sched (Fun.const status) let rec bind (mx : ('a, 'wls) t) (f : 'a -> ('b, 'wls) t) : _ t = - let rec bind_status (x : _ status) (f : _ -> _ status) : _ status = + let rec bind_status (x : _ status) (outter_wls : 'wls) f : _ status = match x with - | Now x -> f x + | Now x -> run (f x) outter_wls | Yield (prio, lx) -> - Yield (prio, Sched (fun wls -> bind_status (run lx wls) f)) - | Choice (mx1, mx2) -> Choice (bind_status mx1 f, bind_status mx2 f) + Yield (prio, Sched (fun wls -> bind_status (run lx wls) wls f)) + | Choice (mx1, mx2) -> + let mx1' = bind_status mx1 outter_wls f in + let mx2' = bind_status mx2 outter_wls f in + Choice (mx1', mx2') | Stop -> Stop in Sched (fun wls -> - let argumented_f x = run (f x) wls in match run mx wls with | Yield (prio, mx) -> Yield (prio, bind mx f) - | x -> bind_status x argumented_f ) + | x -> bind_status x wls f ) let ( let* ) = bind