Lambda the Ultimate

Hi all,

I noticed a similarity between semaphores and other thread-synchronization mechanisms, and control dominators (from control flow theory).

A control dominator is a node that controls the control paths that go through it. Basically, in a control flow graph, if node B post-dominates node A, any path from A to the end-node *must* go through B.

In a similar way, a semaphore guarantees that any path from the wait() call to the end of the execution, *must* go through the signal() call. This feels like "runtime" post-dominance, which is of course a very informal way of putting it.

Does anybody know if there is more research about this similarity? Can dominance be generalized to a runtime concept? Can it help us understand thread-based concurrency better, or is that a lost cause in advance?

We show that it is possible to reconstruct a significant portion of the type information which is implicit in a program, automatically annotate function interfaces, and detect definite type clashes without fundamental changes to the philosophy of the language or imposing a type system which unnecessarily rejects perfectly reasonable programs. To do so, we introduce the notion of success typings of functions. Unlike most static type systems, success typings incorporate subtyping and never disallow a use of a function that will not result in a type clash during runtime. Unlike most soft typing systems that have previously been proposed, success typings allow for compositional, bottom-up type inference which appears to scale well in practice.

A recent paper using a subset of Erlang for the examples. This continues the trend of methods for uncovering type errors in dynamically-typed Erlang. One such tool, Dialyzer, is now part of the Erlang distribution.