4 ms·

I don't have time to read it in full right now, but a quick glance over that paper doesn't show any formalisation of data races, which is specifically what that

by dbaupp 10y ago

I don't have time to read it in full right now, but a quick glance over that paper doesn't show any formalisation of data races, which is specifically what that parenthetical is about, not just general "concurrency safety". Having a detailed description of concept seems important because Rust is fairly precise in what it defends against, possibly giving the programmer more flexibility and power than in a system that attempts to solve many problems (but of course giving them less assistance when writing something that fits within the rules of the more defensive languages). Of course, it's possible that a language "accidentally" solves that problem without it having been formalised, it just seems less likely.

nickpsecurity 10y ago
It's in the disk buffer and monitor examples. Here's a relevant quote: "A disk buÆer is a data structure shared by two concurrent processes. The details of how such a buÆer is constructed are irrelevant to its users. All the processes need to know is that they can send and receive data through it. If they try to operate on the buÆer in any other way it is probably either a programming mistake or an example of tricky programming. In both cases, one would like a compiler to detect such misuse of a shared data structure." "To make this possible, we must introduce a language construct that will enable a programmer to tell a compiler how a shared data structure can be used by processes. This kind of system component is called a monitor. A monitor can synchronize concurrent processes and transmit data between them. It can also control the order in which competing processes use shared, physical resources." Sounds like he understands the problem is concurrent processes stepping on each others toes using a shared, data structure. He has nice drawings and charts to go with it. Plus, an early model to solve it statically at compile time. Jweb_Guru noted some limitations of his method but it understands and solves the fundamental problem. Hansen's own work improved on it later plus it was obsoleted by things like Ravenscar, SCOOP and now Rust's method. Nice that he had a whole OS protected from concurrency errors at compile time in the 70's, though. :)
- dbaupp 10y ago
  None of that looks like a formalisation or even a description of a data race, at least not in the modern sense.
  - nickpsecurity 10y 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.
    - dbaupp 10y ago
      I'm not looking for a formal mathematical model or anything, just a precise plain English description of a data race (not a race condition), e.g. like the following: 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.)
      - 10y ago

by dbaupp 10y ago

nickpsecurity 10y ago

It's in the disk buffer and monitor examples. Here's a relevant quote: "A disk buÆer is a data structure shared by two concurrent processes. The details of how such a buÆer is constructed are irrelevant to its users. All the processes need to know is that they can send and receive data through it. If they try to operate on the buÆer in any other way it is probably either a programming mistake or an example of tricky programming. In both cases, one would like a compiler to detect such misuse of a shared data structure." "To make this possible, we must introduce a language construct that will enable a programmer to tell a compiler how a shared data structure can be used by processes. This kind of system component is called a monitor. A monitor can synchronize concurrent processes and transmit data between them. It can also control the order in which competing processes use shared, physical resources." Sounds like he understands the problem is concurrent processes stepping on each others toes using a shared, data structure. He has nice drawings and charts to go with it. Plus, an early model to solve it statically at compile time. Jweb_Guru noted some limitations of his method but it understands and solves the fundamental problem. Hansen's own work improved on it later plus it was obsoleted by things like Ravenscar, SCOOP and now Rust's method. Nice that he had a whole OS protected from concurrency errors at compile time in the 70's, though. :)

dbaupp 10y ago
None of that looks like a formalisation or even a description of a data race, at least not in the modern sense.
- nickpsecurity 10y 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.
  - dbaupp 10y ago
    I'm not looking for a formal mathematical model or anything, just a precise plain English description of a data race (not a race condition), e.g. like the following: 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.)
    - 10y ago