A Science of Concurrent Programs [pdf]
lamport.azurewebsites.netIt's appropriate that this is appearing at the death of Niklaus_Wirth. He really was the first to get serious about formalizing concurrency. P and V, and all that.
This feels very retro. I used to work on this sort of thing, but that was back in the early 1980s. This reads like something from back then, when people were first figuring out how to think about concurrency.[1] That's how people thought about this back then.
There's been progress in the last four decades. There are completely different approaches, such as symbolic execution. The Microsoft Static Driver Verifier is an example. There's also a theory of eventually-consistent systems now, with conflict-free replicated data types. It's also more common today to think about concurrency in terms of messages rather than variable access, which is easier to reason about. There's also more of a handle on the tooling problem. Not enough of a handle, though. Proof of correctness software still hasn't really gone mainstream. (In IC design, though...)
There's a tendency in this area to fall in love with the notation and formalism, rather than viewing it as a means for making better software. In practice, most of the things you need to prove in program proving are trivial, and have to be mechanized or you never get anything done. Once in a while, a theoretically difficult problem shows up. You need some way to address those abstractly and feed the results back into the semi-automated system.
The main concurrent problem addressed in this paper is the Paxos algorithm. That's similar to the earlier arbiter problem.[2] The arbiter problem is also about resolving who wins access to a shared resource in a parallel system. It's down at the hardware level, where two processors talk to one memory, and has to be resolved in nanoseconds or less. There's no sound way to select a winner in one round. But, for each round, you can tell if the algorithm has settled and produced a winner. You have to iterate until it settles. There's no upper bound on how many rounds it takes, but it is statistically unlikely for it to take very many. Arbiters were the first hardware device to have that property, and it was very upsetting at the time. Multiprocessor computers were built before the arbiter problem was solved, and they did indeed have hardware race conditions on access to memory. I used to debug operating systems for those things, and we did get crashes from that.
Good to see someone is still plugging away on the classics.
[1] https://archive.org/details/manualzilla-id-5928072/mode/2up
> He really was the first to get serious about formalizing concurrency. P and V, and all that.
The computer science of concurrency began with Dijkstra, not Wirth. And it was Dijkstra who introduced the P and V semaphore operations [1].
[1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD01xx/E...
Geez, he did that too? I'm on a concatenative language chat server (you know, Forth, Joy, Factor, Kitten and the like), and someone recently realized one of his earliest papers from 1962 is one of the first to highlight the generality of stack-based languages. Like it's already halfway there towards a proper Forth.
[0] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD00xx/E...
Oops, right.
One person I rarely hear mentioned did similar work: Per Brinch Hansen. He built OS’s with Concurrent Pascal and Edison. His papers are below for those curious:
First thing I see after opening a random paper[0]:
> Three decades ago, Dijkstra (1960) proposed the standard method of dynamic memory allocation for recursive procedures in block structured, sequential languages, such as Algol 60 (Naur 1963), Pascal (Wirth 1971) and C (Kernighan 1978).
Sheeesh, Dijkstra, can you please not show up everywhere like you're the Euler of computer science for FIVE MINUTES?!
Seriously though, that looks like a very interesting collection, will have to search through that in more detail later. Also curious about SuperPascal[1]. The first release/latest stable release column on the wiki page is kinda funny[2].
[0] http://brinch-hansen.net/papers/1995c.pdf
Section 1.2 has an essential warning for many Hacker News readers!
"You probably belong to one of two classes of people who I will call scientists and engineers. Scientists are computer scientists who are interested in concurrent computing. If you are a scientist, you should be well-prepared to decide if this book interests you and to read it if it does.
"Engineers are people involved in building concurrent programs. If you are an engineer, you might have a job title such as programmer, software engineer, or hardware designer. I need to warn you that this book is about a science, not about its practical application. Practice is discussed only to explain the motivation for the science. If you are interested just in using the science, you should read about the language TLA+ and its tools, which are the practical embodiment of the science [27, 34]. But if you want to understand the underlying science, then this book may be for you."
There's a line between the discovered stuff and the invented stuff. I always love to see it spelled out in different ways.
I tell my students that you can understand And rediscover the science part by understanding basic principles, by applying mathematical logic.
While the engineering part you need to learn, as the engineering decisions are full of conventions and constraints of the time of invention and the people inventing.
But understanding the science and knowing roughly the constraints gets you very far. There are usually only a few superficialities left, like concrete syntax, that are basically impossible to "understand" and need to be "learned".
Is there? When it comes to math and abstract concepts such as these I can see no such line. To me it seems e.g. the real numbers were invented about as much as they were discovered. Same goes for the semaphore.
(Of course the exact syntax and semantics of let’s say semaphores in POSIX belong to a different category. But I’m not sure I’d want to call it an “invention”.)
Well, the examples so do fall more under the abstractly provable side of things when it comes to their behavior.
But take the Sieve algorithm that was posted yesterday[0], or Powersort[1] (Timsort with its bugs fixed). To some degree those are more engineering discoveries about which algorithm behaves best with real-world data. Although Powersort actually involves a lot of formal maths to prove it does not have degenerate edge-cases, so maybe I should have stuck with Timsort.
This is a much-debated question in the philosophy of mathematics.
One of the stronger arguments that the real numbers were discovered, rather than invented, is their “unreasonable effectiveness” in aiding our exploration and understanding of the physical world.
The same can’t be said for equally abstract but clearly invented concepts such as the rules of chess.
I think it’s a mixture of both, but using its ability to explore the physical world as the benchmark seems myopic because math can be used to describe universes other than our own. Our universe just happens to be the one we focus on because that part of mathematics is particularly interesting, but if anything it means the structures we put in place to manage that aspect are invented not discovered.
Also from Leslie Lamport is this amusing course on TLA+ which is a good intro into Formal Specifications.
Posted yesterday: https://news.ycombinator.com/item?id=38859393
The thing that always confused me about concurrency and multithreading problems is the fact that books either are too practical(programming examples) or too theoretical(Lamport), they never have a good balance.
Does anyone have a suggestion for a good book? It should discuss CAS and how it's implemented on hardware level as a bare minimum.
This is Science. Computer Science. From one of the greatest alive.
"This is a preliminary version of a book. If you have any comments to make or questions to ask about it, please contact me by email. But when you do, include the version date. I expect there are many minor errors in this version. (I hope there are no major ones.) Anyone who is the first to report any error will be thanked in the book. If you find an error, please include in your email your name as you wish it to appear as well as the version date."
People often mistake software engineering, or IT with computer science.
Those are not science.
The main exception might be high-assurance systems. They require clear description of requirements, formal specification of design + goals, proof one embodies the other, test cases that show it empirically, replication by third parties, and hostile review (pentesting) of all of that.
Praxis’ method was a practical application of these concepts used in industry:
https://www.anthonyhall.org/Correctness_by_Construction.pdf
If the design is the hypothesis, would you count that as science?
Is computer science even science? It feels like we should have called ourselves computationally-applied mathematicians.
Funny you ask this question, since yesterday there was a HN post about Herbert Simon.
Here is Allen Newell, Alan Perlis, and Herbert Simon's response (1967) to your question about whether computer science is even science. For context, the three of them are Turing Award winners and early pioneers of computer science. https://www.cs.cmu.edu/~choset/whatiscs.html
Professors of computer science are often asked: "Is there such a thing as computer science, and if there is, what is it?" The questions have a simple answer:
Wherever there are phenomena, there can be a science to describe and explain those phenomena. Thus, the simplest (and correct) answer to "What is botany?" is, "Botany is the study of plants." And zoology is the study of animals, astronomy the study of stars, and so on. Phenomena breed sciences.
There are computers. Ergo, computer science is the study of computers. The phenomena surrounding computers are varied, complex, rich. It remains only to answer the objections posed by many skeptics.
...
It is a side effect on how it is called in US and some other english speaking coutries I guess.
What people in US call computer science, in Portugal is a math degree major, mostly called something like Computing Applied Maths.
Computer related degrees are called Informatics Engineering, where computer science subjects are mixed with software engineering content, the degree is certficied by Engineerings Order, and is protected professional title.
Or you have Business Informatics, more tailored to current software being used in companies with little theory, more focused in management stuff.
Very similar in Italy as well, where the math side is just called Informatics and the engineering side Informatics Engineering. The former is typically part of the hard maths department, the latter of Engineering. There is significant overlap of course, and both degrees allow being professionally certified by the Engineering Order.
It’s as much a science as mathematical physics, I would suppose? You can make predictions (scaling of an algorithm, correctness of a concurrent algorithm) and test them empirically.
Some people might call pure math a “science”, but this is at the very least applied math (ie more connected to physical reality than pure math).
You could, but this book doesn't, as far as I've skimmed.
It even makes the case as to why not:
> This usually means that there are an enormous number of possible executions, and testing can examine only a tiny fraction of them.
I like to call it non-material science :) Sure call it math, but studying information and computation gets into what is logically or combinatorically possible, the nature of chaos and symmetry. not just a little system of manmade manipulable symbols.
I'm reminded of the first lecture in SICP[0] :)
There are plenty of parts of CS that qualify as a science, like HCI, empirical aspects of networking and systems research, empirical parts of ML, etc.
You are right. It should be called Computation.
Computer science is not a science; it's a form of math (which is not science).
i see Tony Hoare is referenced, but no mention of Bill Roscoe and his bottom
https://www.cs.ox.ac.uk/people/bill.roscoe/publications/1.pd...
”This is not the place for modesty. I was very good at concurrency.” Agreed!
This will go down as the most legendary sentence by a legendary computer scientist.