Vaughan asks
How might a logic based on sets of traces deal with each of the
following situations?
1. Distinguish the race implicit in a|b from the race-free situation
implied by ab+ba.
2. Reason about observations made by a team of distributed observers
who agree on what events happened but not in what order.
3. Reason about the possible interleavings of two concurrent sine
waves. (Presumably one falls back on some other technique for
combining traces than interleaving them.)
The answer is that I don't know and I don't care. These questions
never arise in my work.
How can it be that I find these issues to be irrelevant when Vaughan,
who's an intelligent and (generally :-) reasonable computer scientist,
considers them important? To answer this, I must begin with a
discussion of the nature of science.
Any science is ultimately concerned with the real world. A scientific
theory consists of a mathematical formalism together with a way of
relating that formalism to the real world. For example, Newtonian
mechanics consists of a mathematical theory of point masses moving
along trajectories in mathematical 3-space, together with a way of
relating those mathematical objects to the motions of real objects,
such as planets. Note that not every concept in the mathematcal
formalism need correspond to something in the physical reality--for
exaample, the vector potential of classical electromagnetism has no
physical counterpart.
Any useful scientific theory has a limited domain of application. A
theory-of-everything is generally good for nothing. Newtonian
mechanics can't describe the flow of fluids, for which one needs a
theory containing mathematical concepts corresponding to friction and
viscosity.
For computer science, the real world usually consists of computers
(hunks of wire and silicon) executing programs. Theories in computer
science are based on such diverse mathematical formalisms as Turing
machines, temporal logic, and CCS.
To judge a scientific theory, one must know what its claimed domain of
applicability is. The work of mine that I mentioned in an earlier
message involves a theory whose domain is the specification and
verification of functional properties of concurrent systems. I won't
describe this domain here, except to note that "functional properties"
include eventual termination and upper and lower time bounds on
termination; they exclude probability of termination and expected time
to termination.
Computer scientists have tended to be vague about the domain of
applicability of their theories. As a result, people who work in one
theory often think their theory is good for everything. For example, I
have heard people say that the algebraic laws of CCS make it good for
verifying distributed algorithms. CCS works fine for verifying biscuit
machines. It is hopelessly impractical for verifying even the simplest
distributed spanning tree algorithm, let alone the more complex
algorithms that system builders use. Robin Milner realizes this (I've
discussed it with him), but many of his disciples don't.
This doesn't mean that CCS is worse than my theory; just that it has a
different domain of applicability. It is as silly to say that CCS is
better or worse than my theory as it is to say that physics is better
or worse than biology. Human nature being what it is, almost all
physicists believe in their hearts that physics is more important than
biology. However, physicists understand that not everyone believes
this, so a university will teach biology even if the dean of faculty is
a physicist. One wishes that computer scientists were as
understanding.
I think there are two general reasons why a concept that's important to
theory A may be absent from theory B:
(i) The concept is irrelevant to the domain of applicability of
theory B.
(ii) The concept belongs to the mathematical formalism of theory A
and, even though the two theories have overlapping domains of
applicability, theory B's method of translating reality into
mathematical formalism makes the concept irrelevant or
meaningless.
Case (ii) is the more insidious cause of misunderstanding. People get
so used to their favorite theory that they confuse its mathematical
formalism with physical reality. For example, some advocates of CCS
will say that my theory is deficient because it doesn't distinguish
between internal and external nondeterminism. They don't realize that
internal/external nondeterminism is part of the mathematical formalism
of CCS, not a property of physical reality, so there is no reason why
it should be a meaningful concept in another theory. This error is not
confined to one side of any ideological fence. A colleague of mine
once asserted that he could prove any kind of property of a program,
since he could prove safety and liveness properties and any property is
the conjunction of a safety and a liveness property. He was confusing
the real-world concept of a property (in "prove any kind of property")
with the mathematical concept of a property as a set of behaviors (in
"any property is the conjunction ...").
It can be argued that (ii) is an unavoidable source of
misunderstanding, since one can discuss physical reality only in terms
of mathematical models. I don't think the situation is so hopeless.
We can make statements about the physical world like "if you press this
key, then the system crashes" that mean approximately the same thing to
everyone, regardless of his philosophical persuasion.
I think that Vaughan's question 3 (sine waves) is an example of (i) and
his question 2 (teams of observers) is an example of (ii). His
question 1 (race conditions) is more interesting and warrants
discussion.
A race condition is bad if it makes the circuit behave incorrectly.
When verifying circuits, one is interested only in proving that a
circuit behaves correctly, not that it behaves incorrectly. So, one
never has to prove the existence of a race condition. The
specification of the circuit describes its external behavior, and a
race condition is something that happens inside the circuit. So,
proving the absence of a race condition is never a primary goal. If
there is a potential race condition that never actually occurs--for
instance, because of the initial conditions--then the proof will
contain a lemma (a mathematical formula) whose physical interpretation
will be the absence of a race condition.
However, the concept of a race condition is not irrelevant. A race
condition on its inputs might cause a circuit component to produce an
invalid output voltage--a "1/2" instead of a "0" or a "1". In this
case, a mathematical model of the component that allows only the
outputs "0" and "1" is inadequate. With such a model, the domain of
applicability of the theory would not include the actual circuit.
Fortunately, with more sophisticated models (for example, by including
a "1/2" output), I believe it is possible to use my theory to reason
about real circuits. (I haven't done such reasoning myself, but others
have using similar theories.) The concept of a race condition is
relevant for modeling the real circuit in the mathematical formalism,
but it doesn't appear in the formalism itself.
Scientific theories are useful because the mathematical formalism is
simpler than physical reality. Newtonian physics eliminates an awful
lot of important details--like you and me--when it represents the earth
as a point mass. Those details are irrelevant for computing planetary
orbits. They are not irrelevant for studying human history. Science
is the art of simplification.
A theory should be as simple as possible, but no simpler.
- Albert Einstein
The test of a scientific theory is how well it helps us understand
and/or manipulate the real world.
I will close with a word about mathematics. Many computer scientists
aren't scientists at all; they're mathematicians. They work in the
domain of mathematical formalism, with no concern for its application
to the real world. That's fine. The world needs pure mathematicians
as well as scientists. But it's important for mathematicians to
realize that they're not scientists. Number theorists don't criticize
Newtonian mechanics for using real numbers rather than integers.
Computer-scientist/mathematicians should be equally sensible.