I
fondly remember Dijkstra! He inspired important advances in my own
professional development as related in this posting. I was fortunate to
have stimulating conversations. Interactions with Dijkstra were
generally very focused on solutions he had recently found or problems he
was trying to solve.
Dijkstra was a physicist turned programmer--a pragmatist to the core who used mathematical tools when needed to solve problems. My background in mathematics has made my
work more in the framework of mathematical abstraction applied to practical issues.
When working on the same issues, our approaches (and solutions) come from
different perspectives. Pragmatism and abstraction are both useful in research.
Listening to Dijkstra
and reading his publications was always worthwhile even though we often
disagreed. I learned a great deal from him and very much appreciate having
interacted with him and observed him in action.
One
of the finest tributes to Dijkstra is to
take his work seriously. One on one, Dijkstra loved a good debate! This
posting further develops some of his most important work.
Dijkstra's semaphores were a major advance in concurrent
programming. Dijkstra used semaphores to implement critical sections of code in
which activity in the section excludes all other activities from executing in
the section. In large programs, semaphores are not easy to manage. Bugs
in the use of semaphores (also known as "locks") have caused many irreproducible
crashes in large software systems. A region of mutual exclusion is a generalization
of a critical section that protects local variables in addition to code. As
initially developed, regions of mutual exclusion are less powerful than using
semaphores. A "hole" in a region of mutual allows an activity to
temporarily leave the region and later return to exclude other activities. Regions
with holes provide a structured way to have the full power of semaphores, without
allowing their dangerous use. Consequently, system crashes can be prevented
using regions of mutual exclusion with holes.
Global
states are central to the Church/Turing model of
computation. In this model, there is a global state with
nondeterministic transition
to the next state. A state transition can be initiated by a computation
step
that specifies that one of a number of specified steps can be executed
next. The
model has the property of bounded nondeterminism. Bounded nondeterminism
means
that there is a bound determined in advance for the number of
possibilities that
a system can explore given that it must always come back with an answer.
In the development
of a theory of concurrent computation, Dijkstra remained committed to a
global
state model of computation. This commitment gave rise to the “unbounded
nondeterminism” controversy. Digital systems can be physically
indeterminate by
making use of arbiters in order to resolve reception order in
communication
between systems. Because of physical indeterminacy, a digital system can
have
the property of unbounded nondeterminism in that no bound exists when it
is started on the number
of possibilities that an always-responding digital system can explore.
Being restricted to bounded nondeterminism is one the reasons that the
Church/Turing model of computation is inadequate
for digital computation. More
general models of computation had to be developed beyond the
Church/Turing model.
The upshot was that Dijkstra and I agreed to disagree on the issue of
physical
indeterminacy and consequent unbounded indeterminacy.
Following 1951 work by Alan Turing, Dijkstra developed a
theory of computation based on attaching predicates to global states in his wonderful
book "A Disciple of Programming". He formulated preconditions for predicates
in the nondeterministic transition from one nonlocal state to its
successor, which systematized Turing's earlier work.
An induction principle was implicit in Dijkstra's theory
of computation. Because global states do not exist in the theory of digital
computation, the induction principle for proving properties of digital computation
must be based on computational events rather than global states. The induction
principle for digital computation is analogous to the one that Dedekind
developed for the natural numbers. To prove that a predicate P holds for every
natural number, Dedekind's induction principle has two steps as follows:
- Base step: Prove that P holds for 0.
- Induction Step: Prove that if P holds for natural number n,
then it holds for n+1.
Dedekind proved that his induction principle rigorously characterizes
the natural numbers. Analogously, to prove that a predicate P holds for every event
of a digital system, event induction has two steps as follows:
- Base step: Prove that P holds for every incoming event of
the system.
- Induction step: Prove that if P holds for an event e, then it
holds for each event that immediately follows e.
Many kinds of properties
of digital computation can be proved using event induction. Event induction can
be used to prove that a particular digital system will always respond to a
request. Also, it can be used to prove that a particular digital system will
always have a some invariant property viewed from outside even as the system
changes its behavior over time. Unlike the Church/Turing model, the event induction
principle rigorously characterizes digital computation.
Dijkstra's concurrent
automatic storage reclamation algorithm is a marvel. It causes no pauses in
operation of a system and causes no pause between ending one phase of
reclamation and beginning the next phase. However, Dijkstra's algorithm does
not compactify storage. Instead, storage is reclaimed in pieces throughout
memory. Consequently, the algorithm does not maintain locality of reference,
which is crucial to performance on modern computer cores. Inspired by his algorithm,
Henry Lieberman and I published a paper on generational automatic storage
reclamation in which storage is divided into generations by time of creation
and use of storage. In practice, the most recent generation has much better
locality of use.
Dijkstra's work on
self-stabilizing systems helped inspire new developments in Intelligent
Systems. The intuition is that a system should be stable even in face of disagreement
about empirical information, which is extremely common in an Intelligent System.
Classical logic can make absurd inferences using such information even
if disagreement is deeply hidden. The absurd inferences can be used in
cyberattacks against Intelligent Systems. Unlike classical logic, robust
inference can prevent absurd inferences being made using empirical information.
Consequently, robust inference is crucial to the development and universal deployment
of Intelligent Systems in this decade.
