Categories
systems theory

Are threads evil? (updated)

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]

 

Categories
academics software security theory

Dijkstra versus Perlis (updated)

Bertrand Russell.
Bertrand Russell.

Dijkstra wrote:

He [Perlis] published a very obnoxious paper arguing against a mathematical approach to programming cite

The paper  by De Millo, Lipton and Perlis  starts as follows:

Many people have argued that computer programming should strive to become more like mathematics. Maybe so, but not in the way they seem to think. The aim of program verification, an attempt to make programming more mathematics-like, is to increase dramatically one’s confidence in the correct functioning of a piece of software, and the device that verifiers use to achieve this goal is a long chain of formal, deductive logic. In mathematics, the aim is to increase one’s confidence in the correctness of a theorem, and it’s true that one of the devices mathematicians could in theory use to achieve this goal is a long chain of formal logic. But in fact they don’t. What they use is a proof, a very different animal. Nor does the proof settle the matter; contrary to what its name suggests, a proof is only one step in the direction of confidence. We believe that, in the end, it is a social process that determines whether mathematicians feel confident about a theorem–and we believe that, because no comparable social process can take place among program verifiers, program verification is bound to fail.

To me, the problem with Dijkstra is that he was so sharp and such a good writer that he was able to make persuasive cases out of obviously wrong ideas. Dijkstra wanted to be a scientist in the model of theoretical physics, not an engineer. I’m pretty confident that Dijkstra was wrong: programming is engineering – in fact, physics is not as far from engineering as some people would like to believe. I’m not a huge fan of the engineering discipline as it exists in the USA. It has all sorts of negative aspects – including those Dijkstra railed against. But the vision of a programmer as, not a mathematician, but a formal logician flying far above the grubby compromises and trade-offs of mere engineering in a platonic bubble of pure reasoning is wrongheaded.

Dijkstra published some criticism of the Demillo paper at the time and in their response the authors stated something that, as far as I know, remains true

We must begin by refusing to concede that our confidence in a piece of real software has ever been increased by a proof of its correctness

When I was in graduate school (a long time ago), a famous formal methods sctandem_mugholar came for a talk and explained to us that formal methods were needed if we were ever going to develop fault tolerant software. I pointed out that, for example, the Tandem Software worked pretty well in practice. “It cannot”, retorted the famous scholar.

So there.

Here’s Edsger Dijkstra discussing the birth of the use of axiomatics in computer science – the start of “formal methods” research.  What’s striking is the assumed choice between “axiomatic” and “mechanistic” as if there was no other way. In a later note he writes:

And now we are back at our old dilemma. Either we take by definition all properties of the model as relevant, or we specify in one way or another which of its properties are the relevant ones. In the first case we have failed to introduce in the name of “divide et impera” an interface that would allow us to divide and rule and the study of how we could build upon the (only implicitly defined) interface seems bound to deteriorate into a study of the model itself; in the second case we are again close to the axiomatic method….

[…]

Or, to put it in another way: if the traditional automata theory tends to make us insensitive to the role interfaces could and should play in coping with complex designs, should it then (continue to) occupy a central position in computing science curricula?

And I’m struck by the idea  that seems utterly wrong to me, that one either uses the methods of formal logic OR one is stuck without any ability to abstract or underspecify,  And it’s also interesting to see this impoverished view of automata theory that underpins so much of the formal methods literature.

The reason mathematics has advanced so much was not because of the Euclidean axioms-lemma-theorem straitjacket, but in spite of it. Luckily, when we actually discover mathematics, we do it the Babylonian way, empirically and algorithmically. It is only when it is time to present it, that we put on the stifling Greek formal attire.

so says Doron Zeilberger

 

Updated:  with minor format improvements 2/16/2016 and merged with an earlier article 10.2.2016 Erev RH.

Categories
operating systems state maps

more on missed wakeup

Here are some conventions [Update: typos fix, Friday]

  • We are concerned with state machines and sequences of events. The prefixes of a sequence include the empty sequence “null” and the sequence itself.
  • Relative state: If “w” is the sequence of events that have driven a system of state machines from their initial to their current state then
    • |M is the output of state machine “M” in the current state (reached by following input sequence “w” from the initial state of M)
    • a|M is the output of M in the state reached from the current state by an “a” event.
    • z|M is the output of M in the state reached from the current state by the sequence of events “z” (if it is not clear from the context whether “z” is an event or a sequence, then we can just say which it is.)
  • Absolute state where the sequence parameter is made explicit. This is mostly useful fordefining the initial output and for when we construct composite state machines.
    • w:M is the output of state machine “M” in the state reached by following input sequence “w” from the initial state of M.
    • wa:M is the output of M in the state reached by following the sequence wa (obtained by appending event a to sequence w) from the initial state of M.
    • wz:M is the output of M n the state reached by following the sequence wz (obtained by appending event sequence z to sequence w) from the initial state of M (if it is not clear from the context whether “z” is an event or a sequence, then we can just say which it is.)
    • null:M is the output of M in its initial state.

Specific state machines

  • |Time is the current real-time.
  • |Running(p) =1 if p is executing and 0 otherwise
  • |Runnable(p) =1 if p wants to be scheduled, 0 otherwise.
  • |RequestWakeup(p,e)=1 if p is requesting a wakeup on event e, 0 otherwise
  • If |Runnable(p)=0 then a|Running(p) ≤ |Running(p) (if p is not runnable it can stop running, but not start running.)
  • If a|Runnable(p) > |Runnable(p) then there is at least one e so that a|RequestWakeup(p,e)< |RequestWakeup(p,e) (a process can only become runnable if some wakeup event happens and is cleared.)
  • If a|RequestWakeup(p,e) < |RequestWakeup(p,e) then a|Running(p)=1 (a request is only cleared if the process is actually made runnable)
  • If |RequestWake(p,e) then there is a t so that whenever z|Time ≥ |Time +t then Sum(prefixes u of z; u|Runable(p)) > 0 (if a process has requested a wakeup, it will become runnable in some bounded time – This liveness criteria is not strictly necessary)
  • Define |Safe(p) by null:Safe(p)=1 and
    • a|Safe(p)=

      • 0 if a|Running(p)=0 and a|Runnable(p)=0 and there is no e so that a|RequestWakeup(p,e) (real trouble requires that we are not runnable so can never start running unless we become runnable and cannot become runnable because we have no requests outstanding).
      • |Safe(p) otherwise (|Safe(p) does not change otherwise)
  • So what we want is to ensure that |Safe(p)=1. If a process requests a wakeup, then deschedules, and then gets a wakeup, everything is fine. The ordering is critical. If the wakeup happens before the process deschedules, but it is committed to descheduling then the process gets in trouble. If the code looks like Request e; sleep; then a wakeup event in-between the two operations is trouble. Note that Request e; if requeststill pending then sleep; is not safe unless the test and the sleep are atomic in some sense. Define |RequestOrder(p) by null:RequestOrder(p)=idle and
    • a|RequestOrder(p) =
      • requesting if |RequestOrder(p) = idle and a|RequestWakeup(p,e)>|RequestWakeup(p,e) for some e.
      • idle if a|Runnable(p) < |Runnable(p) and |RequestOrder(p)=requesting
      • error if a|Runnable(p) < |Runnable(p) and |RequestOrder(p) != requesting
      • |RequestOrder(p) otherwise.
  • |RequestOrder(p) != error does not ensure |Safe(p).
  • One solution is a lock. Suppose (Property L) If |locked(p)>0 then a|Running(p) = Running(p) and a|RequestWakeup(p,e) >= |RequestWakeup(p,e). That is, the lock prevents a running process from not running and prevents events from clearing requests -but we can make a process not-runnable while it holds the lock. Redefine RequestOrder to watch the lock.
    • a|RequestOrder(p) =
    • errror

      • if a|Locked(p) <|Locked(p) and RequestOrder(p) != (Ready or Idle)
      • or if a|Runnable(p) <|Runnable(p) and RequestOrder(p) != ready
    • locked otherwise if |RequestOrder(p) = idle and a|Locked(p) > |Locked(p) .
    • requesting otherwise if |RequestOrder(p)=locked and a|RequestWakeup(p,e)>|RequestWakeup(p,e) for some e
    • ready otherwise if a|Runnable(p) < |Runnable(p) and |RequestOrder(p)=requesting
    • idle otherwise if a|Locked(p) < |Locked(p) and |RequestOrder(p)=ready
    • |RequestOrder(p) otherwise.
  • Given Property L, |RequestOrder(p) != errror does assure |Safe(p).
Categories
algebra

Data structures and algebra

[Edited 9/10] There’s an easy connection between data structures and basic abstract algebra that may or may not mean anything, but keeps getting rediscovered. I’ve never seen it clearly explained (anyone with a reference or who notices an error in my rusty algebra- please send me a note! A discrete note would be nice -) ).

What keeps on getting rediscovered is that objects with invertible and commutative methods would make things very convenient especially for transactions and for concurrent access. What I have not seen explained is that this discovery reflects the distinction between groups and monoids.

A monoid is one of the simplest algebraic structures and is usually given as a set M of elements and and a binary operation \(\circ\) on elements of M with the following properties:

  • Closure: for every a and b in M, \(a \circ b\in M \).
  • Associative:    \(a \circ  \) \(( b \circ c ) \) = \((a \circ b) \circ c \) for every a, b, and c in M
  • Identity: M contains an element I so that for every \( a \in M, I \circ a = a \circ I =a \).

That’s it. A pair \((M,\circ)\) and three conditions: closure, associativity and identity. The natural numbers 0,1,2,… form a monoid with ordinary integer addition as the operation and 0 as the identity. The positive numbers form a monoid with 1 as the identity and multiplication as the operation. More intriguingly for our purposes, the methods of an abstract data type or object generate a monoid.

A monoid \( (M, \circ)\) is “generated” from a set X if and only if X is a subset of M and every element of M can be constructed from elements of X using the operation. For example, the monoid of non-negative integers with addition as the operation can be generated from \(\{0,1\}\) since \(2= 1+1, 3 = (1+1)+1\) and so on. One really simple type of monoid is the set \(E^*\) of all finite strings that can be generated from an alphabet with string concatenation as the operator.

We can use the methods of an object as the generators of a monoid as follows. Let’s define an object by a set V of possible values and a set F of methods that can act on the object. A method is really just a function from V to V so that if the object has value v and we apply method f the object value becomes f(v). The binary associative operation of “function composition” can be used to construct “programs” from methods: \(f (gh))(v) = f(g(h(v)))\). The monoid generated by the methods, then, is the set of programs that can be constructed using function composition on the methods. All we have to do further is insist that there is a null method \(Null(v)= v\) is in F.

For example, if our data structure is a stack and our methods are \(push_v\) for every v in some set of values V, plus pop, add (pop the top two values, add and push the result), sub, dup, swap, and \(null\), we can build a Forth Monoid.

If a is an element of a monoid and there is a second element b so that \(a \circ b = I\)  then b is called the “inverse” of a. If there is an inverse for every element of the monoid, then the monoid is called a “group”. (Note that in a group if b is the inverse of a, then a is the inverse of b because of associativity. If the group operation commutes, the group is called Abelian or commutative.

Most monoids are not groups. For example, our Forth Monoid has an inverse for “dup” (“pop” ) but pop does not have an inverse for a very interesting reason: pop loses information. Add has no inverse for the same reason: if the stack is (100,200) and an add method produces (300), then there is no operation that will deduce magically that 100 and 200 were on the stack before and not (0,300) or (1,299) or …  Monoids that are not groups lose information when they compute programs. If an object is associated with a group, then no matter what the starting value of the object, if we know the program that was applied to the object, we can produce (in theory) an anti-program that returns us to the initial state. An example of an object that generates a group is an incrementer with the single method “add1” with values over the set 0 – (232 -1) The inverse of add1 is sub1 which can be generated by 232 add1’s (note that  the words “efficient” or “practical” did not appear anywhere above).

It has been noticed more than once that data structures whose monoids are groups would be easier to parallelize or to use for transactions. For example, if programs can be inverted: so that for every program p there is a -p with -pp = I then we can unroll back to earlier states. That is, if we apply f,g,h to the data structure, and then realize that the transaction cannot be completed, we know that \(-h(-g(-f(f(g(h(x)))))) = x\). We do not have to know what “x” was to undo the transactions. If the programs “commute”, life is even easier, since undoing a single method application can be done at any time, without undoing other method applications. With a little thought you can see that a commutative group data structure is convenient for parallel computation because the order of operations doesn’t matter (less synchronization required) and because every operation is reversible. So if Task T starts modifying the data structure and more important task K interrupts, T’s partially completed changes to the data structure can be rolled back and K can do what it needs.

I’m not completely convinced that stumbling into group theory tells us anything useful about data structures except that computer science is hard and is mostly concerned with horribly irregular structures that do not possess convenient properties. But groups and monoids keep popping up in computer science, even though theoretical CS people seem to not be interested anymore. Famously, state machines determine monoids (or semi-groups) and there is a body of mathematics called Krohn-Rhodes theory which is concerned with factoring monoids into cascades of groups and residual monoids that correspond with splitting state machines into pipelines that have no feedback. Also there is a nice relationship between logging and group structure: Most data structures cannot be practically converted into group like structures even though every monoid can be made into a group by adding a log.

Suppose we make our Forth object have values (data-stack,log-stack) where the log-stack is essentially a stack of data removed from the stack so that “pop” removes the top element of the stack and pushes it onto the log stack – then “invert-pop” can pop the log-stack and push the value onto the data stack. I wonder if “bounded invertibility” would be an interesting property. The interesting Forth objects have a bounded stack anyways. Suppose we add a smaller log-stack so we can invert some programs: suppose the methods are invertible and programs constructed by composing at most K methods are invertible.

Anyways, there is something worth digging out in all this: think of filesystems designed to be K-deep group-like.

(I was inspired or provoked to produce this note after attending a talk by Maurice Herlihy at UT. I can’t say I understood much of Professor Herlihy’s talk (my fault, not his) but he was discussing the utility of converting data structure monoids to groups without mentioning either groups or monoids. I also found out that distributed shared memory is still around- how depressing.)