You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I think ARCs call into the runtime to do atomic operations. Now that we have atomic intrinsics, we can use those instead.
I suspect some of the nasty organization in pipes might have been working around compiler bugs, like #3005. The workarounds may not actually be effective though, it could have just been stuff I tried when looking for a workaround that I never removed.
I think this is closable now (see #5042, #6732, #6740). We have a good atomics library now, arcs use them and/or the atomic intrinsics, and pipes use the atomic intrinsics. Reopen if you disagree.
Workflows that run the perf regressions (`scripts/kani-perf.sh`) do not
need to build Kani, as the perf script itself builds Kani in release
mode:
https://github.com/model-checking/kani/blob/dc0978043c52492112e4ad37a617fd3c8100ef1f/scripts/kani-perf.sh#L12
The extra build step was causing Kani to be built two extra times for
the `benchcomp` flow because the workflow was building it in debug mode,
so the script will end up rebuilding it in release mode. This should
save about 3 minutes for the `benchcomp` flow.
nasty organisation in pipes and in arc.
The text was updated successfully, but these errors were encountered: