Communicating Sequential Processes (Hoare/Davies 2004)
1–10 of 17 posts
Re: Communicating Sequential Processes (Hoare/Davies 2004)
#2ok, I read the preface and while I was blasted out by the pretentiousness of the final line, I am interested about the content. However, I can't seem to get an overall 'what the hell is this useful for?' summary. The first part of the preface is all just abstract 'you will become better'.
Can someone please enlighten me? I think Hoare is great and would like to know if this stuff would benefit me as a programmer.
Re: Communicating Sequential Processes (Hoare/Davies 2004)
#3ok, I read the preface and while I was blasted out by the pretentiousness of the final line, I am interested about the content. However, I can't seem to get an overall 'what the hell is this useful for?' summary. The first part of the preface is all just abstract 'you will become better'. Can someone please enlighten me? I think Hoare is great and would like to know if this stuff would benefit me as a programmer.
One direct influence that CSP has had was on the design of the concurrency features of Go:
In general, things like CSP and related formalisms like Petri Nets are used to build mathematical models of systems so that properties of these systems can be proved. However, they have also influenced a lot of real-world software designs - I've worked on software that controlled large scale industrial systems (cement mills) that used Petri Nets both to represent processes but also to prove properties of these processes.
A watered down version of Petri Nets also formed the basis for UML Activity Digrams - if you like that kind of thing. CSP also influenced the design of the Transputer and the Occam programming language.
[NB People using the bars in Activity Diagrams as a means of joining lines up rather that as their actual meaning (starting and stopping concurrent activity) drives me round the bend, but most of UML does that...]
Edit: I guess it's an interesting question as to when actually knowing CS formalisms like CSP actually helps. I guess my response would be: lots of real world systems we need to analyse, control and/or build exhibit lots of complex behaviour. What's our main tools for modelling complex domains: maths. CSP is just one neat way of applying mathematical reasoning (either to structure understanding or to actually prove stuff) to concurrency. Whether you need to know this or not to be a good developer is another question - 99% probably don't.
Edit2: Note that just because I have a superficial familiarity with these concepts doesn't mean I would label myself a "good developer"!
Re: Communicating Sequential Processes (Hoare/Davies 2004)
#4ok, I read the preface and while I was blasted out by the pretentiousness of the final line, I am interested about the content. However, I can't seem to get an overall 'what the hell is this useful for?' summary. The first part of the preface is all just abstract 'you will become better'. Can someone please enlighten me? I think Hoare is great and would like to know if this stuff would benefit me as a programmer.
Distributed systems are really hard. This line has been endlessly parroted and, also, endlessly reproven. They are really hard.
The major reason why they're hard is that your standard reasoning toolbox is insufficient. Understanding distributed systems means being aware of a much larger state space and how things like special relativity impact it (I'm being a bit flippant, but not actually inaccurate—message latency is not poorly modeled by special relativity). Most programmers use reasoning methods like operational modeling (single threaded), guess-and-check, and unit testing. These are simply completely insufficient.
If you want to model full distributed systems you might want to use something like algebraic topology. It's a useful tool for understanding the entire state space of a system and its valid transitions. It can be used to prove Paxos or Raft are correct. https://www.ideals.illinois.edu/bitstream/handle/2142/33762/...
Another method is to simplify a whole lot what a "distributed system" is and hope to find a more analyzable model where more standard reasoning tools work. CSP is one of these. It's a simpler model where some of the reasoning tools of regular formal languages can be used to understand its operation.
The upshot is that CSP won't be as powerful as you could imagine possible when building a distributed system, but it'll be massively more manageable so long as its sufficient for your goals. It's, as such, formed the basis for some popular distributed tools like Erlang.
Re: Communicating Sequential Processes (Hoare/Davies 2004)
#5ok, I read the preface and while I was blasted out by the pretentiousness of the final line, I am interested about the content. However, I can't seem to get an overall 'what the hell is this useful for?' summary. The first part of the preface is all just abstract 'you will become better'. Can someone please enlighten me? I think Hoare is great and would like to know if this stuff would benefit me as a programmer.
One way of testing/verifying concurrent programs is to build a model of the program, and then see if the model satisfies certain properties. This is fairly tedious and does not scale very well. However, while it wont prove anything, it can be useful to build some kind of model; it can often point out some flaws in the design that you missed.
All in all, I think its sort of like a programmer learning the basics of discrete math. You're not actually learning how to program but it can change the way you think. Obviously, if you go to deep (which perhaps CSP is) you might get a bit off track.
Re: Communicating Sequential Processes (Hoare/Davies 2004)
#6ok, I read the preface and while I was blasted out by the pretentiousness of the final line, I am interested about the content. However, I can't seem to get an overall 'what the hell is this useful for?' summary. The first part of the preface is all just abstract 'you will become better'. Can someone please enlighten me? I think Hoare is great and would like to know if this stuff would benefit me as a programmer.
Distributed systems are really hard. This line has been endlessly parroted and, also, endlessly reproven. They are really hard. The major reason why they're hard is that your standard reasoning toolbox is insufficient. Understanding distributed systems means being aware of a much larger state space and how things like special relativity impact it (I'm being a bit flippant, but not actually inaccurate—message latency…
You reminded me of this - http://www.informit.com/articles/article.aspx?p=1768317
There are some interesting differences between CSP and Erlang (and Go, which arguably implements CSP a bit more closely than Erlang).
Re: Communicating Sequential Processes (Hoare/Davies 2004)
#7CSPs are also implemented in Clojure's core.async
This blog post helped me understand some use cases for CSP
http://swannodette.github.io/2013/07/12/communicating-sequen...
Re: Communicating Sequential Processes (Hoare/Davies 2004)
#8ok, I read the preface and while I was blasted out by the pretentiousness of the final line, I am interested about the content. However, I can't seem to get an overall 'what the hell is this useful for?' summary. The first part of the preface is all just abstract 'you will become better'. Can someone please enlighten me? I think Hoare is great and would like to know if this stuff would benefit me as a programmer.
It is also used in evolutionary biology to model evolving and cooperating agents.
Re: Communicating Sequential Processes (Hoare/Davies 2004)
#9I remember as a student that I was comfortable just looking at notation and reasoning about things. CSP has a very simple notation.
But after a decade as a professional programmer, I somehow lost patience for things that can't be run. Either experience taught me not to trust things that don't run, or ideas are not fun unless you can poke at them, or my mind got lazy. I just want to run things and see what happens.
I like the CSP model, but since nothing can be run in this book, unfortunately I would look elsewhere to study it.
I've been playing with Standard ML and it seems like a nice way to mathematically specify algorithms, but which can still also be run.
Also, Leslie Lamport's style of doing mathematics with runnable proofs seems very interesting: http://scholar.google.com/scholar?cluster=145533208090118123...
Re: Communicating Sequential Processes (Hoare/Davies 2004)
#10I remember as a student that I was comfortable just looking at notation and reasoning about things. CSP has a very simple notation. But after a decade as a professional programmer, I somehow lost patience for things that can't be run. Either experience taught me not to trust things that don't run, or ideas are not fun unless you can poke at them, or my mind got lazy. I just want to run things and see what happens. I…
I think they're two different UXen on two different reasoning methodologies: equational versus interactive. Time spent in Haskell where both are predominant has taught me that when used in synchrony they both have their place, but I agree there's a weakness in using equational alone: it creates great concepts but they are so substantially weakened by "operationalization" that there's still a huge risk.