4 ms·
Have you heard of TLA+? If not, I suggest checking it out. It's kinda made to handle investigating and preventing such rare race conditions.
by namibj 5y ago
Have you heard of TLA+? If not, I suggest checking it out.
It's kinda made to handle investigating and preventing such rare race conditions.
- im_down_w_otp 5y agoThat 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.