3 ms·
can we have a "formal semantics for multi-threading" ? why it's not a thing?
by dgan 4y ago
can we have a "formal semantics for multi-threading" ? why it's not a thing?
- baq 4y agoIt’s super duper hard, mostly.
- kjeetgill 4y agoThere are. They're called memory models. I know Java's is pretty readable (see below). I think C and C++ have them too now. But when you're building on these things there's always lots of room to get them wrong! [0]: https://en.wikipedia.org/wiki/Java_memory_model https://en.wikipedia.org/wiki/Java_memory_model [1]: https://docs.oracle.com/javase/specs/jls/se18/html/jls-17.html#jls-17.4 https://docs.oracle.com/javase/specs/jls/se18/html/jls-17.ht...
- tsimionescu 4y agoAnother poster shared the Java memory model, and C++ and C have them as well. The article we're discussing shows another kind of formal model for multithreaded code in TLA+, and actually uses it to investigate this bug. There is also Tony Hoare's Communicating Sequential Processes formal model, first presented in 1978; and an entire field of CS research called process calculus. So, pick a formal model and use it - though note that formal methods tend to add significant extra effort to use, and may or may not pay off depednig on your domain and desired outcomes.