|
|
|
|
|
by nickpsecurity
3547 days ago
|
|
Im not a concurrency expert. Just had basic explanations and training common with other developers. How it was explained to me was two or more tasks trying to simultaneously access a shared resource for reading or writing. These accesses might not happen in the desired order, causing incorrectness. Then there were lock-related issues on top of that. Hansens work formalized what I just described in terms of English, diagrams, and compiler checks. He started with sequential operations on private data in modules. He says if two or more share thd same private data they might not execute in desired order. The monitor pattern enforced user-specified order on function calls to shared data. Built-in to language & compiler. If my description of race conditions is inaccurate or insufficient, I'd appreciate a link to one that you think is more accurate that I could use as a comparison point against the Hansen paper. Otherwise, his description of problems implementing concurrency sounds exactly like what I learned in books on multithreading, supercomputing, etc. Shared resource used in incorrect order due to concurrency. Note: Also, his colleagues Dijkstra and Hoare were still inventing and developing formal verification at the time. Tooling sucked. Standard practice, like he did with Algol and COBOL compilers, was writing things like this in precise English with code examples or diagrams. Not sure if you were expecting a HOL model or something when you said "modern" but I figured Id mention stuff was primitive then. |
|
A data race is when
- two threads access a single memory location,
- at least one of which is a write, and
- at least one of which has no synchronisation^
(^ synchronisation in the sense of things like atomic instructions, not necessarily full locks.)