Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove sideg list from sync return value #211

Merged
merged 5 commits into from
May 10, 2021
Merged

Remove sideg list from sync return value #211

merged 5 commits into from
May 10, 2021

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Apr 30, 2021

Previously sync transfer functions returned both the updated state (like every other transfer function), but also an assoc list of sidegs to perform. Since sync may just use sideg directly to make the same side effects to global unknowns, the returned list provides no additional value. It's there for historical reasons.

Therefore I see no value keeping it around. Its removal simplifies a lot of sync code, especially in BasePriv and Constraints.

@sim642 sim642 added the cleanup Refactoring, clean-up label Apr 30, 2021
@sim642
Copy link
Member Author

sim642 commented Apr 30, 2021

One might have the performance concern that by doing sideg directly instead of collecting them causes some solver side effect functions to fire immediately, not at the end of the sync transfer. However, this doesn't actually happen because MCP2 for whatever reason collects sidegs anyway and does them together afterwards, including ones from different analyses:

let sync (ctx:(D.t, G.t, C.t) ctx) reason =
let spawns = ref [] in
let splits = ref [] in
let sides = ref [] in
let emits = ref [] in
let f post_all (n,(module S:MCPSpec),d) =
let ctx' : (S.D.t, S.G.t, S.C.t) ctx =
{ local = obj d
; node = ctx.node
; prev_node = ctx.prev_node
; control_context = ctx.control_context
; context = (fun () -> ctx.context () |> assoc n |> obj)
; edge = ctx.edge
; ask = query ctx
; emit = (fun e -> emits := e :: !emits)
; presub = filter_presubs n ctx.local
; postsub= filter_presubs n post_all
; global = (fun v -> ctx.global v |> assoc n |> obj)
; spawn = (fun l v a -> spawns := (v,(n,l,a)) :: !spawns)
; split = (fun d es -> splits := (n,(repr d,es)) :: !splits)
; sideg = (fun v g -> sides := (v, (n, repr g)) :: !sides)
; assign = (fun ?name _ -> failwith "Cannot \"assign\" in sync context.")
}
in
n, repr @@ S.sync ctx' reason
in
let d, q = map_deadcode f @@ spec_list ctx.local in
do_sideg ctx !sides;
do_spawns ctx !spawns;
do_splits ctx d !splits;
let d = do_emits ctx !emits d in
if q then raise Deadcode else d


I noticed in the past (while implementing and tracing #183) that even though MCP2.do_sideg does this grouping, it didn't and still doesn't seem to properly work. I've identified a tricky interaction between ctx and query which is behind this phenomenon (some side effects bypassing the collection and going to the solver immediately. Since that's an orthogonal issue, I'll be opening a separate PR.

@sim642 sim642 mentioned this pull request May 4, 2021
@sim642 sim642 merged commit 4d68fc3 into master May 10, 2021
@sim642 sim642 deleted the sync-side branch May 10, 2021 09:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cleanup Refactoring, clean-up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants