|
|
|
|
|
|
by dmytroi
2302 days ago
|
|
|
Started using it at work, mostly to verify lock-free code. After verifying a new code for multi producer multi consumer (MPMC) lock free queue, tests were still not passing on iOS in debug... So trust in the model allowed us to start asking if compiler was broken, and ... it was, apparently in Apple's fork of llvm, as they don't really use upstream llvm as-is, 128-bit atomic compare exchange (DCAS) is broken in debug in Xcode 8. In general it is quite useful exercise to even just model existing code line-by-line and see what possible states it can have. I'm still learning though, next step would be to try TLAPS. |
|
|