[nickpsecurity]

"which seems to be a concept only really formalised in the late 80s"

http://brinch-hansen.net/papers/1975a.pdf

http://brinch-hansen.net/papers/

His first, concurrent OS was RC 4000 in 1969. It had many mechanisms in place. He got the key parts of the safety problem figured out by 1972. His language to handle much of it statically at compile-time was done in 1975. His Boss 2 system same year used coroutines + similar concepts to run 100 activities at a time with a proof of deadlock freedom. Finally, he used Concurrent Pascal to implement Solo system which ran its processes safely without using physical, memory protection. These summaries came from "Evolution of Operating Systems" on 2nd link.

So, the stuff was well-established by the mid-70's with operating systems using it in production. Just ignored by mainstream like a lot of good stuff for various reasons. ;)

[dbaupp]

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]

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]

None of that looks like a formalisation or even a description of a data race, at least not in the modern sense.

[nickpsecurity]

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]

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.)

[nickpsecurity]

Alright that's clear. It's also in the first paper I gave you in the first illustration. The problem you're having is you've constrained the definition of concurrency or race conditions to only be about the language common among application programmers, esp threading. Concurrency is broader than that: it can apply to processes, threads, systems, protocols, or even hardware circuits. All that is required is two or more active things working with a shared resource in a way where operations might get interleaved and out of order in a way that makes computation incorrect.

Knowing that, Hansen starts on problem with RC4000 (1969) describing protecting communication between "processes" via message buffers, message queues, and checks performed on them to ensure validity. That and Dijkstra's critical regions are where the foundations were laid. His next step was the formalization the problem in 1972:

http://brinch-hansen.net/papers/1972a.pdf

Section's 1 and 2 cover basics of concurrent operation + race conditions. It was clear to me by the abstract but should be extra clear he's talking about them by this statement about Algorithm 1:

"The copying, output, and input of a record can now be executed concurrently. To simplify the argument, we will only consider cases in which these processes are arbitrarily interleaved but not overlapped in time. The erroneous concurrent statement can then be executed in six different ways with three possible results."

That's definitely a concurrency error. He then talks about mutual exclusion and synchronization with an await primitive. Closer to modern language but the focus on operating systems in the early 1970's means he says processes instead of threads and things like disk buffers or message queues instead of shared memory. Although his examples in 1972 paper are clearly shared memory since it's at algorithm level.

So, they discovered the problem around late 60's, implemented an early solution for sharing resources among processes in 1969, fully described race conditions + some other stuff by 1972, had a safer-by-design language to catch it at compile time by 1975, and applied that to implement a concurrent, production OS (Solo) for day-to-day use by academics by 1976.

So, race conditions were both formalized and initially solved in early to mid 1970's. I don't know how much more you need given they had an OS running 100 jobs/users at once interacting on shared resources without visible failures using their concurrency model. Mainstream OS's and apps are still having race conditions pop up on occasion. Clearly, what they were doing was addressing root cause if no race conditions occurred after a successful compile of "multiprogrammed" apps. :)

[gpderetta]

> Just ignored by mainstream like a lot of good stuff for various reasons. ;)

This paper introduced Monitors. It was of course hugely influential.

Mutex and condition variables, the building blocks of monitors made their way into posix threads and from there into C++11.

I believe Java is a much closer realization of Hansen model as every java object is a Monitor.

[nickpsecurity]

Good point. I should qualify that statement better. Hansen's model was statically guaranteeing freedom from issues at compile time. There were projects aiming at that which could've implemented a similar model but didn't. More work could've gone into eliminating its limitations, etc. The Ada and Eiffel people carried the torch, though, with interesting progress. Now Rust is. Ada folks aren't resting, though, as ParaSail is pretty neat.

[Jweb_Guru]

This system does not support recursion. It also does not have to reason about atomics and so on because it is not intended for multicore systems; indeed, it assumes that all access is serialized through a mutex, and doesn't consider the existence of types like single-threaded reference counters (like Rust's Rc). It is describing threads with exclusive access, and a scheduling mechanism for waiting on locks, but the mechanism is entirely dynamic (and the paper assumes the existence of a virtual machine, which is frequently invoked to deal with tricky cases).

Some relevant lines:

> A Concurrent Pascal compiler will check that the private data of a process only are accessed by that process. It will also check that the data structure of a class or monitor only is accessed by its procedures

is significantly less than what Rust provides, because:

> Processes cannot operate directly on shared data. They can only call monitor procedures that have access to shared data. A monitor procedure is executed as part of a calling process (just like any other procedure).

> If concurrent processes simultaneously call monitor procedures that operate on the same shared data these procedures will be executed strictly one at a time. Otherwise, the results of monitor calls would be unpredictable. This means that the machine must be able to delay processes for short periods of time until it is their turn to execute monitor procedures. We will not be concerned with how this is done, but will just notice that a monitor procedure has exclusive access to shared data while it is being executed.

Rust allows shared access to immutable data and does not require either serialization or the invocation of a virtual machine; it also allows nondeterministic operation to be used as long as it cannot cause memory unsafety.

Additionally, there are other, more basic things that the system is not capable of. For instance:

> (Strictly speaking, a compiler can only check that single monitor calls are made correctly; it cannot check sequences of monitor calls, for example whether a resource is always reserved before it is released. So one can only hope for compile time assurance of partial correctness.)

A major part of what Rust brings to the table is the ability to statically avoid problems like use after free and double free even in a concurrent setting. How would I avoid resource leaks in a system like this without a per-thread allocator (which would likely prevent sending across threads)?

Of course, it's not clear to me that this matters anyway, since I can't destroy a thread or shared data structure!

> Dynamic process deletion will certainly complicate the semantics and implementation of a programming language considerably. And since it appears to be unnecessary for a large class of real-time applications, it seems wise to exclude it altogether. So an operating system written in Concurrent Pascal will consist of a fixed number of processes, monitors, and classes. These components and their data structures will exist forever after system initialization.

I agree that people have a strong tendency to not know what past work has been done, and Concurrent Pascal is admirable, but what Rust does is not the same thing. Rust specifically tackles a lot of hard problems in concurrency that simply do not exist as long as you (1) assume away deallocation for shared data structures, and (2) serialize all access to those data structures.

(There are lots of other specific points I could go into; for instance, Concurrent Pascal apparently lacks facilities for generic programming, so I probably couldn't combine two correct concurrent data structures and expect a third correct concurrent data structure to come out. But that stuff isn't directly related to concurrency).

[nickpsecurity]

"I agree that people have a strong tendency to not know what past work has been done, and Concurrent Pascal is admirable, but what Rust does is not the same thing. "

I'm not saying it does. The claim I replied to said preventing things like data races was done till well into the 80's. I showed systematic investigations of the problem plus a production solution had been done by mid-70's. You've nicely showed how far ahead methods like Rust got. ;)

[dbaupp]

> The claim I replied to said preventing things like data races was done till well into the 80's

No, it definitely didn't: it said data races as a concept seemed to not be formalised until the late 80's.

[nickpsecurity]

The word formalized might be where disagreement started. If you meant precise & useful, Hansen formalized the definition Ive seen in some books. If you mean in mathematical specification, you might be correct. Im not sure when that got started.