Skip to content

WIP: expose number of idle cores

Björn Brandenburg requested to merge idle-cores into master

What do you think of this way of defining work-conservation in a way that transparently works for both uni- and multiprocessor platforms?

To me, this looks appealing. The only downside that I see is that in proofs one doesn't get to destruct the exists j_other right away (i.e., we'd need a few helper lemmas to establish that idle_in s == 0 implies exists j_other.

We could also keep both notions and establish equivalency of the two definitions (once for each processor model).

CC: @sbozhko @mlesourd @sophie

Merge request reports