6 ms·

Teaching Concurrency (2009) [pdf]

151 points by luisfoliv 10y ago

argv_empty 10y ago
The only actionable advice in here for someone tasked with developing a curriculum for teaching concurrency is to make sure the prerequisite courses instill the idea of computation as a sequence of state transitions.
- Const-me 10y ago
  “Sequence of state transitions” implies you can order them by time. Generally, various state transitions happen in parallel, their relative order is undefined even on an SMP system. You can serialize the transitions if you want, but that usually costs performance. This is especially true for distributed parallel computing, where the state is also distributed.
  - argv_empty 10y ago
    It sounds like you're modeling the state space wrong. In a concurrent system, the state is not just one thread's (or one processor's, or one machine's) internal data (including program counter). That would be like saying a (single-threaded) program's state is the contents of the registers and topmost stack frame. The state in a concurrent system is the combination of every thread's internal state. And what actually happens is a sequence of such arrangements. One arrangement is not realized without replacing the previous one.
    - Const-me 10y ago
      I’m aware the state you were talking includes state of all threads. When you combine several sequences of state transitions (one sequence per thread), you don’t get another sequence of state transitions. When two CPU cores perform two state transitions at the same time, you typically cannot determine whichever of those transitions happened first. We might have different definitions what’s sequence. I mean this: https://en.wikipedia.org/wiki/Sequence https://en.wikipedia.org/wiki/Sequence As you see, global order is required for bunch of elements (in this case, state transitions) to form a sequence. And in concurrent and especially parallel programming, there’s no global order for those transitions. Hence, those transitions don’t form a sequence.
      - argv_empty 10y ago
        No, we just have different notions of system state. If we have a pair of, say, Turing machine heads on one tape that aren't necessarily moving in lockstep, I say that the system state is the tape contents, the two heads' locations, and the two heads' states. A transition for this system can be either or both heads moving either direction, overwriting the symbol they're pointing at, and changing its own internal state. The state {tape="000111000", head0loc=0, head0state=2, head1loc=4, head1state=6} might transition to {tape="000101000", head0loc=0, head0state=2, head1loc=5, head1state=2}, or it might transition to {tape="100111000", head0loc=1, head0state=2, head1loc=4, head1state=6}, or to {tape="100101000", head0loc=1, head0state=2, head1loc=5, head1state=2}. In a given run of the system, one of those is what actually happens. Then another happens after that, and so on. So we get a sequence of them. A transition is not one machine head changing its position and state. {head0loc=0, head0state=2}->{head0loc=1, head0state=2} is not a transition because that does not identify a pair of whole-system states.
        Const-me 10y ago
        > one of those is what actually happens No it’s not. If the heads aren’t moving in lockstep, what actually happens is you’ll extremely rarely have a moment of time when both locations are whole numbers. At one moment you have { head1loc=0, head2loc=4.17 }, head #1 reached the cell position on the tape, head #2 is still moving. After a while, you’ll have { head1loc=0.872, head2loc=5}, head #1 is on its way, head #2 reached the cell position. Looks like for a Turing machine with two asynchronously moving heads, there’s no usable concept of “state” at all. That’s very close to what happens when doing actual parallel programming on real hardware. Good luck applying your idea of computation as a sequence of state transitions to that.
        argv_empty 10y ago
        Even if a Turing machine were a physical object (I had thought you would be aware that it's not), either one of those moves completes before the other, or both complete simultaneously.
  - pron 10y ago
    The state transitions can be partially ordered, but the way this works in TLA is that every computation is a set of legal behaviors (sequences of states).
deleted 10y ago
[deleted]
TickleSteve 10y ago
I think the first thing people should be taught about concurrency... is when not to use it. Concurrency can result in increased maintenance costs and complexity. Concurrency is also not more efficient on a single core. Concurrency can help with latency and response time. In embedded systems in particular, there is an over-use of concurrency which often results in bloated, complex code.
- nkozyra 10y ago
  > Concurrency is also not more efficient on a single core. This isn't a hard and fast rule. There is overhead to parallelism.
  - tbrownaw 10y ago
    And if you step out all the parallelism from your concurrency runtime, you get rid of a big chunk of the overhead. But even with purely cooperative single-threaded multitasking, there's still some overhead vs "ordinary" strictly serial code.
  - TickleSteve 10y ago
    For CPU bound code, concurrency is pure overhead. For I/O bound code, concurrency can give you some benefit. ...but in general, people do not analyse this before throwing tasks at a problem.
    - srean 10y ago
      > ...but in general, people do not analyse this before throwing tasks at a problem. Would that be just anecdotal ?
      - TickleSteve 10y ago
        yes... in ~25 years in the business, over ~10 companies. ..and I can tell you that precisely none of them performed a correct analysis of a systems concurrency needs before 'designing' it. A common artifact of this is far too many tasks.
Const-me 10y ago
When I was a kid, I loved playing transport tycoon deluxe videogame. When I grew up to be a programmer, never had much problems with concurrent stuff. IMO designing concurrent programs is conceptually similar to building complex high-throughput low latency railway networks in the game.
- InclinedPlane 10y ago
  Related: https://deadlockempire.github.io/ https://deadlockempire.github.io/
- rdmsr 10y ago
  An open source version (remake?) of the game exists[1]. [1] https://www.openttd.org/en/ https://www.openttd.org/en/
- hcarvalhoalves 10y ago
  Same idea: https://www.factorio.com/ https://www.factorio.com/
fizixer 10y ago
Highly recommended: Allen Downey The Little Book of Semaphores (free pdf here: http://greenteapress.com/wp/semaphores/ http://greenteapress.com/wp/semaphores/)
jasondebo 10y ago
So, what is the inductive invariant in that simple algorithm?
- pron 10y ago
  The inductive invariant is the correctness property itself (when all processes are done then at least one y is 1) in conjunction with "for all processes, when the process is not on line 1, then its x value is 1". You can probably replace the second conjunct with "for all processes, if the x value is 0, then the process is not done", but the proof gets a bit harder.
  - pron 10y ago
    The proof then follows like so, by induction on the states of the program: This is our partial correctness property PartialCorrectness ≜ AllDone ⇒ ∃ p ∈ ProcSet : y[p] = 1 And this is the inductive invariant: Inv ≜ PartialCorrectness ∧ ∀ p ∈ ProcSet : pc[p] ≠ "Line1" ⇒ x[p] = 1 We need to show that Inv implies PartialCorrectness (trivial), that Inv holds in the initial state, and that if it holds in any state s, then it holds in any possible consecutive step s'. It's easy to see that it holds in the initial state. Now, let's assume it holds in s, and prove for s'. To make this transition, some process p either executes line 1 or executes line 2. If it executes 1, then PartialCorrectness doesn't change because no new process is done. The second conjunct holds because we've just left line 1 and x has been assigned (by the definition of line 1). If we are currently in line 2, the second conjunct of the invariant doesn't change. By the definition of this action, we'll be done. Here we have two cases, either we set y to 1, or we set y to zero. If we set y to 1, we're done and PartialCorrectness holds. If we set y to 0 then by the assumption of the invariant, the process we depend on must not be done, hence AllDone is false, and PartialCorrectness holds. QED.

151 points by luisfoliv 10y ago

The only actionable advice in here for someone tasked with developing a curriculum for teaching concurrency is to make sure the prerequisite courses instill the idea of computation as a sequence of state transitions.

Const-me 10y ago
“Sequence of state transitions” implies you can order them by time. Generally, various state transitions happen in parallel, their relative order is undefined even on an SMP system. You can serialize the transitions if you want, but that usually costs performance. This is especially true for distributed parallel computing, where the state is also distributed.
- argv_empty 10y ago
  It sounds like you're modeling the state space wrong. In a concurrent system, the state is not just one thread's (or one processor's, or one machine's) internal data (including program counter). That would be like saying a (single-threaded) program's state is the contents of the registers and topmost stack frame. The state in a concurrent system is the combination of every thread's internal state. And what actually happens is a sequence of such arrangements. One arrangement is not realized without replacing the previous one.
  - Const-me 10y ago
    I’m aware the state you were talking includes state of all threads. When you combine several sequences of state transitions (one sequence per thread), you don’t get another sequence of state transitions. When two CPU cores perform two state transitions at the same time, you typically cannot determine whichever of those transitions happened first. We might have different definitions what’s sequence. I mean this: https://en.wikipedia.org/wiki/Sequence https://en.wikipedia.org/wiki/Sequence As you see, global order is required for bunch of elements (in this case, state transitions) to form a sequence. And in concurrent and especially parallel programming, there’s no global order for those transitions. Hence, those transitions don’t form a sequence.
    - argv_empty 10y ago
      No, we just have different notions of system state. If we have a pair of, say, Turing machine heads on one tape that aren't necessarily moving in lockstep, I say that the system state is the tape contents, the two heads' locations, and the two heads' states. A transition for this system can be either or both heads moving either direction, overwriting the symbol they're pointing at, and changing its own internal state. The state {tape="000111000", head0loc=0, head0state=2, head1loc=4, head1state=6} might transition to {tape="000101000", head0loc=0, head0state=2, head1loc=5, head1state=2}, or it might transition to {tape="100111000", head0loc=1, head0state=2, head1loc=4, head1state=6}, or to {tape="100101000", head0loc=1, head0state=2, head1loc=5, head1state=2}. In a given run of the system, one of those is what actually happens. Then another happens after that, and so on. So we get a sequence of them. A transition is not one machine head changing its position and state. {head0loc=0, head0state=2}->{head0loc=1, head0state=2} is not a transition because that does not identify a pair of whole-system states.
      - Const-me 10y ago
        > one of those is what actually happens No it’s not. If the heads aren’t moving in lockstep, what actually happens is you’ll extremely rarely have a moment of time when both locations are whole numbers. At one moment you have { head1loc=0, head2loc=4.17 }, head #1 reached the cell position on the tape, head #2 is still moving. After a while, you’ll have { head1loc=0.872, head2loc=5}, head #1 is on its way, head #2 reached the cell position. Looks like for a Turing machine with two asynchronously moving heads, there’s no usable concept of “state” at all. That’s very close to what happens when doing actual parallel programming on real hardware. Good luck applying your idea of computation as a sequence of state transitions to that.
        argv_empty 10y ago
        Even if a Turing machine were a physical object (I had thought you would be aware that it's not), either one of those moves completes before the other, or both complete simultaneously.
- pron 10y ago
  The state transitions can be partially ordered, but the way this works in TLA is that every computation is a set of legal behaviors (sequences of states).

deleted 10y ago

[deleted]

TickleSteve 10y ago

I think the first thing people should be taught about concurrency... is when not to use it. Concurrency can result in increased maintenance costs and complexity. Concurrency is also not more efficient on a single core. Concurrency can help with latency and response time. In embedded systems in particular, there is an over-use of concurrency which often results in bloated, complex code.

nkozyra 10y ago
> Concurrency is also not more efficient on a single core. This isn't a hard and fast rule. There is overhead to parallelism.
- tbrownaw 10y ago
  And if you step out all the parallelism from your concurrency runtime, you get rid of a big chunk of the overhead. But even with purely cooperative single-threaded multitasking, there's still some overhead vs "ordinary" strictly serial code.
- TickleSteve 10y ago
  For CPU bound code, concurrency is pure overhead. For I/O bound code, concurrency can give you some benefit. ...but in general, people do not analyse this before throwing tasks at a problem.
  - srean 10y ago
    > ...but in general, people do not analyse this before throwing tasks at a problem. Would that be just anecdotal ?
    - TickleSteve 10y ago
      yes... in ~25 years in the business, over ~10 companies. ..and I can tell you that precisely none of them performed a correct analysis of a systems concurrency needs before 'designing' it. A common artifact of this is far too many tasks.

Const-me 10y ago

When I was a kid, I loved playing transport tycoon deluxe videogame. When I grew up to be a programmer, never had much problems with concurrent stuff. IMO designing concurrent programs is conceptually similar to building complex high-throughput low latency railway networks in the game.

InclinedPlane 10y ago
Related: https://deadlockempire.github.io/ https://deadlockempire.github.io/
rdmsr 10y ago
An open source version (remake?) of the game exists[1]. [1] https://www.openttd.org/en/ https://www.openttd.org/en/
hcarvalhoalves 10y ago
Same idea: https://www.factorio.com/ https://www.factorio.com/

fizixer 10y ago

Highly recommended: Allen Downey The Little Book of Semaphores (free pdf here: http://greenteapress.com/wp/semaphores/ http://greenteapress.com/wp/semaphores/)

jasondebo 10y ago

So, what is the inductive invariant in that simple algorithm?

pron 10y ago
The inductive invariant is the correctness property itself (when all processes are done then at least one y is 1) in conjunction with "for all processes, when the process is not on line 1, then its x value is 1". You can probably replace the second conjunct with "for all processes, if the x value is 0, then the process is not done", but the proof gets a bit harder.
- pron 10y ago
  The proof then follows like so, by induction on the states of the program: This is our partial correctness property PartialCorrectness ≜ AllDone ⇒ ∃ p ∈ ProcSet : y[p] = 1 And this is the inductive invariant: Inv ≜ PartialCorrectness ∧ ∀ p ∈ ProcSet : pc[p] ≠ "Line1" ⇒ x[p] = 1 We need to show that Inv implies PartialCorrectness (trivial), that Inv holds in the initial state, and that if it holds in any state s, then it holds in any possible consecutive step s'. It's easy to see that it holds in the initial state. Now, let's assume it holds in s, and prove for s'. To make this transition, some process p either executes line 1 or executes line 2. If it executes 1, then PartialCorrectness doesn't change because no new process is done. The second conjunct holds because we've just left line 1 and x has been assigned (by the definition of line 1). If we are currently in line 2, the second conjunct of the invariant doesn't change. By the definition of this action, we'll be done. Here we have two cases, either we set y to 1, or we set y to zero. If we set y to 1, we're done and PartialCorrectness holds. If we set y to 0 then by the assumption of the invariant, the process we depend on must not be done, hence AllDone is false, and PartialCorrectness holds. QED.