4 ms·
That assumes that the problem is in their model, not their implementation.
by im_down_w_otp 5y ago
That assumes that the problem is in their model, not their implementation.
- vlovich123 5y agoIn something like described, it sounds like the design part is where they’re at. If they were optimizing a working algorithm (eg selecting the best memory ordering for some operation), then I’d say they’re in the implementation phase. What’s not clear to me is if TLA+ can properly model the memory model. If I recall correctly, it doesn’t. You’re just testing your logic. That does still leave for some heavy lifting to be done.
- namibj 5y agoAFAIK it can model the interleaving possibilities at hand, and helps to find somewhat short execution traces that violate some logic/assumptions.