This paper by Prof. Edward Lee explains something of why “threads” are such a painful abstraction. As Prof. Lee notes, threads intrinsically create 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.
Consider a really dumb system that keeps a “gain” variable, outputs a single analog voltage, and inputs both an input signal and “messages” that tell it what to do. The input events can be thought of as samples of the analog signals on the “pins”.
Inputs are maps: Pins -> Signals where each input represents one unit of time and the set Pins contains “Vin” and some unknown number of pins (which may not be actual physical pins) comprising the message port.
Given a sequence of inputs, w, we suppose we have a function LastGain(w) that extracts the value of gain we were told to set in the most recent message and SinceLastCommand(w) that counts samples (time units) since the last command message. Let’s be more specific on the “Vin”
LastVin(wa) = a(Vin).
StableVin(wa) = (1+ StableVin(w))*[a(Vin) ==Â LastVin(w)]Â where [exp] is 1 if exp is true and 0 otherwise
Then we can require that Dev(w)= g*v if
StableVin(w)>= t1 and v=LastVin(w)
and g=LastCommand(w) and SinceLastCommand(w) >= t2