This paper by Prof. Edward Lee explains something of why “threads” are such a painful abstraction. As Prof. Lee notes, threads intrinsically create unspecified program operation (which he calls non-determinism) and resource conflicts which we then attempt to “prune” via synchronization and complex tools. In an earlier note, I argued that we should design real-time multi-threaded applications to minimize the need for synchronization, but Prof. Lee goes further to point out that the thread model itself encourages a disorganized program structure. Along those lines, one of the basic difficulties in real-time application design is non-deterministic resource allocation. How can we ever be sure that, for example, a multi-threaded app where threads can allocate memory has sufficient memory for critical threads to proceed?
I’m not a fan of the “algebraic” tagged model that Lee suggests as an alternative – too much of the flavor of “formal methods” via the denotational semantics base. In fact, Liu’s thesis, referenced here, struggles mightly with the unsatisfactory nature of the mathematical framework to get somewhere. Do we really have to create lemmas about posets to describe 2 simple processes? It seems to me that the confusion of the underlying mathematical basis has to be resolved before we can figure this out. Or maybe not.
[partially completed dumb example deleted 2/20/2016]