In article <··············@tti5.uchicago.edu>, Matthias Blume
<····@my.address.elsewhere> wrote:
> In fact, static analysis (although perhaps not in form of type
> systems) is your best (some may say: only) bet against the possibility
> of race conditions and their ilk.
Ironically, I actually agree with this.
E.
···@jpl.nasa.gov (Erann Gat) writes:
> In article <··············@tti5.uchicago.edu>, Matthias Blume
> <····@my.address.elsewhere> wrote:
>
> > In fact, static analysis (although perhaps not in form of type
> > systems) is your best (some may say: only) bet against the possibility
> > of race conditions and their ilk.
>
> Ironically, I actually agree with this.
With Gerard at JPL now, you better agree! :-)
In article <··············@hanabi-air.shimizu.blume>, Matthias Blume
<····@my.address.elsewhere> wrote:
> ···@jpl.nasa.gov (Erann Gat) writes:
>
> > In article <··············@tti5.uchicago.edu>, Matthias Blume
> > <····@my.address.elsewhere> wrote:
> >
> > > In fact, static analysis (although perhaps not in form of type
> > > systems) is your best (some may say: only) bet against the possibility
> > > of race conditions and their ilk.
> >
> > Ironically, I actually agree with this.
>
> With Gerard at JPL now, you better agree! :-)
I've been singing the praises of Spin ever since it was used to catch race
condition bugs in code that I had written. That really knocked my socks
off.
E.
Erann Gat wrote:
> I've been singing the praises of Spin ever since it was used to catch race
> condition bugs in code that I had written. That really knocked my socks
> off.
Any pointers/URLs?
Regards,
Jo
Erann Gat wrote:
> Joachim Durchholz <·················@web.de> wrote:
>
>>Erann Gat wrote:
>>
>>>I've been singing the praises of Spin ever since it was used to catch race
>>>condition bugs in code that I had written. That really knocked my socks
>>>off.
>>
>>Any pointers/URLs?
>
> http://citeseer.nj.nec.com/havelund00formal.html
Thanks, got it, will read it.
> Interestingly, no one brought up the well known (or at least it ought to
> be well known) story of the race condition in the Remote Agent as a
> counterexample to my claim that an undue emphasis on static typing led to
> neglecting what ultimately turned out to be the real problem in the
> billing system, so I'll do it myself.
Not all stories are as widely-known as those involved would want to know.
Actually, static type checking is known to not catch all errors, as the
beaten-to-death Ariane-V crash demonstrated - the failing code was
written in Ada. This time not a race condition but a specification mismatch.
Yet the crash doesn't mean that static type checking is useless.
Anecdotal evidence is easy to come by for any of these issue; it's the
general picture that counts.
Which is why methodological debates are generally fruitless. It's
essentially impossible to do a fair comparison. The best that one can
hope is that it opens new perspectives that weren't seriously considered
before.
It has happened in this discussion - it seems that there's a group of
people who'd like to see static and dynamic checking methods combined,
and there seems to be a rough consensus on what the advantages of such a
system could have. It will be quite exciting if anybody ever casts this
into a serious language.
Regards,
Jo
In article <············@news.oberberg.net>, Joachim Durchholz
<·················@web.de> wrote:
> It has happened in this discussion - it seems that there's a group of
> people who'd like to see static and dynamic checking methods combined,
> and there seems to be a rough consensus on what the advantages of such a
> system could have. It will be quite exciting if anybody ever casts this
> into a serious language.
That would indeed be a most agreeable outcome to this discussion. Surely
there are some Ph.D. students lurking out there who need a thesis topic?
E.
[ Jumping in here at the thread-fork ... I've only peeked at the
discussion so far ]
Joachim Durchholz <·················@web.de> writes:
> Actually, static type checking is known to not catch all errors, as the
> beaten-to-death Ariane-V crash demonstrated - the failing code was
> written in Ada. This time not a race condition but a specification mismatch.
> Yet the crash doesn't mean that static type checking is useless.
Certainly not. The position that reasonable advocates of dynamically
typed languages hold, is that static checks should come second to
rapid development. Once I *think* my code works, I'd like to hear all
the computer can tell me on the issue; until that time, however, I'm
still working ideas out myself, and I want to see my sketches in
action, however sketchy they might be. Even in production code,
sometimes I know things that the static analyzer can't know or can't
figure out, in which case, I want to tell it to make my code work
anyhow. Preferably by telling the analyzer why, but failing that, I
want my code to run.
> Anecdotal evidence is easy to come by for any of these issue; it's the
> general picture that counts.
>
> Which is why methodological debates are generally fruitless. It's
> essentially impossible to do a fair comparison.
Right. If you're solving an already solved (or mostly solved)
problem, systems based on static analysis should win. If you're
trying to solve an unsolved or really difficult or ill specified
problem, dynamic systems have a major edge up. To the extent static
analyzers can understand your approach to the problem, they can help
more than all-dynamic systems.
> The best that one can
> hope is that it opens new perspectives that weren't seriously considered
> before.
>
> It has happened in this discussion - it seems that there's a group of
> people who'd like to see static and dynamic checking methods combined,
> and there seems to be a rough consensus on what the advantages of such a
> system could have.
Ahem, if you haven't already looked at SBCL (recently), I recommend
that you do. It's a Common Lisp implementation that takes static
analysis and the CL type system seriously. It's still very much a
work in progress, and there's a *lot* to do on those fronts, but
IMNSHO, it offers all the benefits of a dynamic language, plus a good
chunk of the benefits of a statically typed one. I'm not saying it's
the Hermetic Substance, but it's an attempt at it.
> It will be quite exciting if anybody ever casts this into a serious
> language.
<rant>
Why does everything have to be its own language? It seems like
everyone who doesn't think this gets ghettoized as Lisp Dialect Foo,
or Smalltalk Dialect Bar ... but the pressure should be the other way
around; the question should not be, "you didn't have anything that
warrented its own language?", but rather, "you couldn't even come up
with a way of integrating your new idea into a useful, existing
language?".
</rant>
Even better, it'd be great if people could come up with practical
systems for doing static analysis directly on object code[*]. Such a
system would not only work with dynamic languages, but it would even
work in the face of compiler bugs. A method of passing (verifiable)
knowledge from the compiler to the verification system, would enable
this approach to be realized to the fullest, with language support
being optional (and very helpful) but not necessary. Then, there's no
need for a new language, and even (!) correct C code could be verified
as correct.
[*] Some readers, especially LispNYC'ers, will realize that such
systems are in fact being worked on. Not only by myself (who gave a
talk on an attempt at such a system at a LispNYC meeting), and my
former research partner, who's now doing graduate work in this area;
but by professors
--
/|_ .-----------------------.
,' .\ / | No to Imperialist war |
,--' _,' | Wage class war! |
/ / `-----------------------'
( -. |
| ) |
(`-. '--.)
`. )----'
From: Joe Marshall
Subject: Re: Why I believe in static analysis
Date:
Message-ID: <oev758m5.fsf@ccs.neu.edu>
···@famine.OCF.Berkeley.EDU (Thomas F. Burdick) writes:
> Certainly not. The position that reasonable advocates of dynamically
> typed languages hold, is that static checks should come second to
> rapid development. Once I *think* my code works, I'd like to hear all
> the computer can tell me on the issue; until that time, however, I'm
> still working ideas out myself, and I want to see my sketches in
> action, however sketchy they might be. Even in production code,
> sometimes I know things that the static analyzer can't know or can't
> figure out, in which case, I want to tell it to make my code work
> anyhow. Preferably by telling the analyzer why, but failing that, I
> want my code to run.
I don't mind static checks that demonstrate `provably bad' code, even
at the experimentation stage. If the compiler notices that (FOO X Y)
can't possibly do anything interesting because X is always a string
and the first thing FOO does is take CAR X, I don't mind the compiler
telling me about this.
A conservative type checker complains if it cannot prove the code
correct, but an `unsound' type checker would complain only if it can
prove the code incorrect. It sure seems to me that unsound type
checking is almost always a good idea (before I get flamed for this by
the static typers, note that sound static type checking is a superset
of the unsound checking.)
Joe Marshall <···@ccs.neu.edu> writes:
>I don't mind static checks that demonstrate `provably bad' code, even
>at the experimentation stage. If the compiler notices that (FOO X Y)
>can't possibly do anything interesting because X is always a string
>and the first thing FOO does is take CAR X, I don't mind the compiler
>telling me about this.
>
>A conservative type checker complains if it cannot prove the code
>correct,
Oh - I thought people were using the opposite definition of
'conservative', that is flags an error only if it can prove the code
incorrect.
>but an `unsound' type checker would complain only if it can prove the
>code incorrect.
And again this is the opposite to what I'd choose: the type checker's
verdict 'there is an error' is unsound if the program might in fact
work.
But I see where you get the names from.
>It sure seems to me that unsound type checking is almost always a
>good idea
But in many cases, the type checker is both sound and complete. I
think this is the case for a simple Hindley-Milner system and for
Haskell (without wacky extensions like Dynamic or things making the
type system unsound or undecidable). I'm not aware of cases where
code is rejected by the type checker but in fact is legal code with a
defined semantics.
Whether you can make your type checker do 'innocent unless proven
guilty' while still catching all real type errors depends on the
language and on what you define as a type error. For Lisp, it would
not be possible to find all and only type errors, though you could
catch many (and perhaps have a few false positives which you choose to
treat as warnings and ignore).
Design a statically-typed language, on the other hand, and it becomes
possible to do what you are asking for and still get maximum benefit
from the machine finding errors in your code before you run it.
--
Ed Avis <··@membled.com>
Ed Avis <··@membled.com> writes:
>But in many cases, the type checker is both sound and complete. I
>think this is the case for a simple Hindley-Milner system and for
>Haskell (without wacky extensions like Dynamic or things making the
>type system unsound or undecidable).
This is usually achieved by defining "completeness" in a rather technical
fashion which does not preclude the existence of a more complete system
that gives a reasonable semantics to programs which are untypeable in the
original system.
>I'm not aware of cases where
>code is rejected by the type checker but in fact is legal code with a
>defined semantics.
This is only because code which is rejected by the type checker is by
definition not legal code. It doesn't necessarily mean that such code
is non-sensical, just that it is not allowed.
Lack of support for polymorphic recursion is a classic example.
--
Fergus Henderson <···@cs.mu.oz.au> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
Fergus Henderson <···@cs.mu.oz.au> writes:
>>I'm not aware of cases where code is rejected by the type checker
>>but in fact is legal code with a defined semantics.
>
>This is only because code which is rejected by the type checker is by
>definition not legal code.
Well, quite. I mean that since the language definition doesn't define
a semantics for such code, you can't really complain that the type
checker would reject it. But you could complain that the language is
unnecessarily restricted by having to take account of type system
limitations when designing new features.
--
Ed Avis <··@membled.com>
Ed Avis <··@membled.com> writes:
>Fergus Henderson <···@cs.mu.oz.au> writes:
>
>>>I'm not aware of cases where code is rejected by the type checker
>>>but in fact is legal code with a defined semantics.
>>
>>This is only because code which is rejected by the type checker is by
>>definition not legal code.
>
>Well, quite. I mean that since the language definition doesn't define
>a semantics for such code, you can't really complain that the type
>checker would reject it.
Consider functions involving polymorphic recursion without an explicit
type declaration. If you look at the Haskell Report, the only sense in
which it does not give a semantics to such functions is that it defines
them to be not type-correct. But otherwise, the semantics is perfectly
clear -- it follows in a quite straight-forward way from the semantics
of function calls. If the restriction in section 4.4.1
"If a variable f is defined without providing a corresponding type
signature declaration, then ... the defining occurrence and all uses
of f within its declaration group must have the same monomorphic type".
was removed, then no other changes would be needed to the Haskell Report
to give a semantics to such functions.
--
Fergus Henderson <···@cs.mu.oz.au> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
Fergus Henderson <···@cs.mu.oz.au> writes:
>Consider functions involving polymorphic recursion without an
>explicit type declaration. If you look at the Haskell Report, the
>only sense in which it does not give a semantics to such functions is
>that it defines them to be not type-correct.
OK, this is a case where the language design is constrained by
worrying about how to type things, and so an example of where static
typing limits the expressivity of the language.
But in most cases, complaining 'the type checker rejected my program!'
is shooting the messenger.
--
Ed Avis <··@membled.com>
Ed Avis <··@membled.com> writes:
>Fergus Henderson <···@cs.mu.oz.au> writes:
>
>>Consider functions involving polymorphic recursion without an
>>explicit type declaration. If you look at the Haskell Report, the
>>only sense in which it does not give a semantics to such functions is
>>that it defines them to be not type-correct.
>
>OK, this is a case where the language design is constrained by
>worrying about how to type things, and so an example of where static
>typing limits the expressivity of the language.
Actually I don't consider this to be a case where static typing limits
the expressivity of the language, because you can express code using
polymorphic recursion in Haskell, you just have to add an explicit
type declaration. So I would just say that this is a case where static
typing slightly increases the verbosity of (a rare subset of) programs.
>But in most cases, complaining 'the type checker rejected my program!'
>is shooting the messenger.
I agree.
It's important to acknowledge the truth of the claim that static type
checkers do reject some valid programs which would be accepted in
a dynamically typed language. My response to such claims is not to
attempt to deny their validity, by defining "program" in such a way as
to make them invalid; instead, I would point out that although these
claims are true, in practice systems it is not a problem, for good modern
type systems, because such cases are rare and it is easy to write such
programs in a way that _is_ acceptable to the static type checker.
--
Fergus Henderson <···@cs.mu.oz.au> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
···@famine.OCF.Berkeley.EDU (Thomas F. Burdick) wrote in message news:<···············@famine.OCF.Berkeley.EDU>...
> <rant>
> Why does everything have to be its own language? It seems like
> everyone who doesn't think this gets ghettoized as Lisp Dialect Foo,
> or Smalltalk Dialect Bar ... but the pressure should be the other way
> around; the question should not be, "you didn't have anything that
> warrented its own language?", but rather, "you couldn't even come up
> with a way of integrating your new idea into a useful, existing
> language?".
> </rant>
Reminds me of what Norvig said in PAIP. It's much better to justify
your work to a PHB by saying "I designed a new language" rather than
"I hacked together a bunch of macros."
Maybe Java preprocessors are in fashion though. I know of one smart
CS prof who lost all interest in Python because he had some problem
installing it once, so he just uses Java. Which you have to admit is
one of the most powerful languages in terms of ease of installation.
Tayss wrote:
> ···@famine.OCF.Berkeley.EDU (Thomas F. Burdick) wrote in message news:<···············@famine.OCF.Berkeley.EDU>...
>
>><rant>
>>Why does everything have to be its own language? It seems like
>>everyone who doesn't think this gets ghettoized as Lisp Dialect Foo,
>>or Smalltalk Dialect Bar ... but the pressure should be the other way
>>around; the question should not be, "you didn't have anything that
>>warrented its own language?", but rather, "you couldn't even come up
>>with a way of integrating your new idea into a useful, existing
>>language?".
>></rant>
>
>
> Reminds me of what Norvig said in PAIP. It's much better to justify
> your work to a PHB by saying "I designed a new language" rather than
> "I hacked together a bunch of macros."
>
> Maybe Java preprocessors are in fashion though. I know of one smart
> CS prof who lost all interest in Python because he had some problem
> installing it once, so he just uses Java. Which you have to admit is
> one of the most powerful languages in terms of ease of installation.
Richard Gabriel has a chapter in his book "Patterns of Software" about
what makes a successful language. Ease of installation, and stuff like
that, are much more important than actual technical details (like
dynamic vs. static typing, and so on ;).
There are two options: either you play that game as well, or you decide
to have something better to do. ;)
Pascal
--
Pascal Costanza University of Bonn
···············@web.de Institute of Computer Science III
http://www.pascalcostanza.de R�merstr. 164, D-53117 Bonn (Germany)
Joachim Durchholz <·················@web.de> writes:
> It has happened in this discussion - it seems that there's a group of
> people who'd like to see static and dynamic checking methods combined,
> and there seems to be a rough consensus on what the advantages of such
> a system could have. It will be quite exciting if anybody ever casts
> this into a serious language.
Indeed, it would be agreable to have a set of analysis and theorem
prover tools to examine and "validate" our codes, and even to help us
generate them from formal specifications. But I see them as much or
more integrated to our editors or our run-times than to our
compilers... I mean that they should not be restricted to the
compilers.
--
__Pascal_Bourguignon__
http://www.informatimago.com/
>>>>> "Erann" == Erann Gat <·········@jpl.nasa.gov> writes:
Erann> (BTW, this is also a counterexample to the theory that you
Erann> can't learn anything from a single data point.)
Well, counterexamples are like that, it only takes one to kill a
theory.
:-)
------------------------+-----------------------------------------------------
Christian Lynbech | christian ··@ defun #\. dk
------------------------+-----------------------------------------------------
Hit the philistines three times over the head with the Elisp reference manual.
- ·······@hal.com (Michael A. Petonic)
Erann Gat wrote:
> Interestingly, no one brought up the well known (or at least it ought to
> be well known) story of the race condition in the Remote Agent as a
> counterexample to my claim that an undue emphasis on static typing led to
> neglecting what ultimately turned out to be the real problem in the
> billing system, so I'll do it myself.
...
> If we had analyzed the entire code base it would have saved us a lot of
> grief. The reason we didn't is because 1) using SPIN is very labor
> intensive and we had a lot of code, so we didn't have time to do it all.
> To use SPIN you have to essentially re-code your algorithm into SPIN's own
> language (PREOMLA). And 2) We thought that if we built a small core that
> was analyzed by SPIN, then we could get away with not analyzing the rest
> of the code as long as it was built on top of this proven-safe core. The
> RA bug showed that this doesn't work in general. (BTW, this is also a
> counterexample to the theory that you can't learn anything from a single
> data point.)
Hmm. So you're saying that using static analysis lulled you
into a false sense of security where you thought that because
you were catching all the bugs of a certain kind (those
in the to-be-proven-safe code that SPIN could catch) you
didn't need to look so hard for other sorts of bugs (those
in other parts of the code, for instance), and one of those
other bugs then caught you?
This is sounding eerily familiar. :-)
--
Gareth McCaughan
.sig under construc
In article <··············@g.mccaughan.ntlworld.com>, Gareth McCaughan
<·····@g.local> wrote:
> Erann Gat wrote:
>
> > Interestingly, no one brought up the well known (or at least it ought to
> > be well known) story of the race condition in the Remote Agent as a
> > counterexample to my claim that an undue emphasis on static typing led to
> > neglecting what ultimately turned out to be the real problem in the
> > billing system, so I'll do it myself.
> ...
> > If we had analyzed the entire code base it would have saved us a lot of
> > grief. The reason we didn't is because 1) using SPIN is very labor
> > intensive and we had a lot of code, so we didn't have time to do it all.
> > To use SPIN you have to essentially re-code your algorithm into SPIN's own
> > language (PREOMLA). And 2) We thought that if we built a small core that
> > was analyzed by SPIN, then we could get away with not analyzing the rest
> > of the code as long as it was built on top of this proven-safe core. The
> > RA bug showed that this doesn't work in general. (BTW, this is also a
> > counterexample to the theory that you can't learn anything from a single
> > data point.)
>
> Hmm. So you're saying that using static analysis lulled you
> into a false sense of security where you thought that because
> you were catching all the bugs of a certain kind (those
> in the to-be-proven-safe code that SPIN could catch) you
> didn't need to look so hard for other sorts of bugs (those
^^^^^^^^^^^^^^^^^^^
> in other parts of the code, for instance), and one of those
> other bugs then caught you?
Not quite. Change "other sorts of bugs" to "the same sort of bug in other
parts of the code" and you are correct.
The reason I think static analysis to find race conditions is more
valuable than static analysis for finding type errors is that empirically
run-time testing seems to be effective at finding type errors, but not at
finding race conditions.
E.
Erann Gat wrote:
> The reason I think static analysis to find race conditions is more
> valuable than static analysis for finding type errors is that empirically
> run-time testing seems to be effective at finding type errors, but not at
> finding race conditions.
I seem to remember seeing some software once designed to help test
for race conditions. Don't remember what it was called. It inserted
random delays into programs to try to trip them up.
David
·········@jpl.nasa.gov (Erann Gat) writes:
>The reason I think static analysis to find race conditions is more
>valuable than static analysis for finding type errors is that
>empirically run-time testing seems to be effective at finding type
>errors, but not at finding race conditions.
Empirically, it takes programmers longer to build and run a test suite
than to hit the 'compile' button. Of course testing will be necessary
eventually, but you may prefer to defer that until you've got the
basic structure of the code clear in your mind (and the compiler's
mechanical checks can be helpful in finding mistakes here). OTOH,
dynamic typing and a language that supports it (eg, elements of a list
can be of different types, not all the same type as in C++ or Haskell)
may save time when you already have test suites constructed, and you
just want to tweak a small corner of the code to try stuff, well aware
that such a change would mean changing other things were you to make
it for real.
--
Ed Avis <··@membled.com>
·········@jpl.nasa.gov (Erann Gat) writes:
> In article <············@news.oberberg.net>, Joachim Durchholz
> <·················@web.de> wrote:
>
> > Erann Gat wrote:
> > > I've been singing the praises of Spin ever since it was used to
> > > catch race condition bugs in code that I had written. That
> > > really knocked my socks off.
> >
> > Any pointers/URLs?
>
> http://citeseer.nj.nec.com/havelund00formal.html
>
> "Formal Analysis of the Remote Agent Before and After Flight"
[snip]
> The Remote Agent was written in Lisp, and it also suffered a
> potentially catastrophic race-induced problem (a deadlock this time)
> in flight. However, there was one significant difference: the race
> condition existed not because we didn't try to find them. We did,
> and in fact the methods that we used to find them were successful.
> However, we only applied them to part of the codebase, and the bug
> turned up in a part of the code that we hadn't analyzed.
I read this paper today--quite interesting. I have a question that's a
bit to the side of the main point of SPIN-style static checking. And
start off by saying that I fully recognize that hindsight is 20-20 and
all that; you guys put Lisp in space and found and fixed this bug
under what must have been tremendous pressure while I had it presented
to me in a paper. So with that caveat, here's my question/observation:
During their clean-room analysis of the bug that actually manifested
during the flight, the SPIN users happened to translate the Lisp code
into Java (in order to be able to feed it into JPF). They came with
something like this:
class Event {
int count = 0;
public synchronized void wait_for_event() {
try { wait(); } catch(InterruptedException e) {}
}
public synchronized void signal_event() {
count = (count + 1) % 3;
notifyAll();
}
}
Now looking at that code I can see immediately that there's a problem
since it doesn't follow the canonical pattern for implementing a
condition variable[1] in Java which would look something like this:
public synchronized void wait_for_event() {
int oldCount = count;
while (count == oldCount) {
try { wait(); } catch(InterruptedException e) {}
}
}
I noticed this immediately because I've written that pattern out about
a zillion times since Java doesn't have actual condition variables and
there's no way to build a condition variable object unless you also
build your own lock object since you don't quite have sufficient
control over the built in monitor locks. (And you don't want to build
your own locks because without macros there's no way to provide a
syntax that guarantees that you always unlock your locks at the end of
blocks the way synchronized blocks do.)
So back when I used to write multithreaded Java code for a living I
wished that I was using Lisp because then I could write a macro to
turn something like:
(wait-for-condition (/= count old-count) lock)
into the appropriate (assuming I already had Lisp versions of Java's
concurrency primitives synchronized and wait):
(synchronized (lock)
(while (not (/= count old-count))
(wait lock)))
I.e. something like:
(defmacro wait-for-condition (condition lock)
(let ((lock-value (gensym)))
(let ((,lock-value ,lock))
`(synchronized (,lock-value)
(while (not ,condition)
(wait ,lock-value))))))
What struck me about the bugs found by the paper's authors is that
they also might have been avoided by using such a macro to abstract
the pattern of a condition variable. Since you *were* using Lisp, in
theory when they found the first batch of bugs (pre flight) someone
could have said--again hindsight is 20-20--hmmm, the real bug here was
that we need to always put the check of the condition we're waiting
for with the actual call to WAIT-FOR-EVENT within a critical section,
let's write a macro to make sure we get that right everywhere.
Do you think this analysis is right or are there complexities that
make such a macro a non-starter?
-Peter
[1] <http://www.acm.org/classics/feb96/>
--
Peter Seibel ·····@javamonkey.com
Lisp is the red pill. -- John Fraser, comp.lang.lisp
In article <··············@javamonkey.com>, Peter Seibel
<·····@javamonkey.com> wrote:
> What struck me about the bugs found by the paper's authors is that
> they also might have been avoided by using such a macro to abstract
> the pattern of a condition variable. Since you *were* using Lisp, in
> theory when they found the first batch of bugs (pre flight) someone
> could have said--again hindsight is 20-20--hmmm, the real bug here was
> that we need to always put the check of the condition we're waiting
> for with the actual call to WAIT-FOR-EVENT within a critical section,
> let's write a macro to make sure we get that right everywhere.
>
> Do you think this analysis is right or are there complexities that
> make such a macro a non-starter?
You are exactly right, and in fact we did have such a macro. Actually, we
had a whole collection of them. That was the "reliable core" that was
analyzed by SPIN.
The problem was one of the application programmers needed a feature for
which we had not implemented a macro, so he rolled his own code and didn't
use a macro. He got the critical sections in all the right places --
except one.
That's the fundamental reason that the "reliable core" concept doesn't
work. There's nothing that prevents you from writing unreliable code on
top of a reliable core if you still have access to synchronizing
primitives.
E.
·········@jpl.nasa.gov (Erann Gat) writes:
> In article <··············@javamonkey.com>, Peter Seibel
> <·····@javamonkey.com> wrote:
>
> > What struck me about the bugs found by the paper's authors is that
> > they also might have been avoided by using such a macro to abstract
> > the pattern of a condition variable. Since you *were* using Lisp, in
> > theory when they found the first batch of bugs (pre flight) someone
> > could have said--again hindsight is 20-20--hmmm, the real bug here was
> > that we need to always put the check of the condition we're waiting
> > for with the actual call to WAIT-FOR-EVENT within a critical section,
> > let's write a macro to make sure we get that right everywhere.
> >
> > Do you think this analysis is right or are there complexities that
> > make such a macro a non-starter?
>
> You are exactly right, and in fact we did have such a macro. Actually, we
> had a whole collection of them. That was the "reliable core" that was
> analyzed by SPIN.
>
> The problem was one of the application programmers needed a feature for
> which we had not implemented a macro, so he rolled his own code and didn't
> use a macro. He got the critical sections in all the right places --
> except one.
>
> That's the fundamental reason that the "reliable core" concept doesn't
> work. There's nothing that prevents you from writing unreliable code on
> top of a reliable core if you still have access to synchronizing
> primitives.
Hmmm. I'm not sure I'd give up on the reliable core concept that
easy--if you've defined a core that you belive covers all the needs of
the folks who are supposed to be using, it ought to be fairly
straightforwerd (either by automation or simply by good practice) to
make sure that no one is using the primitives outside the core. I
would assume people who are writing software that's going to fly in
space can be relied on not to use unexported symbols. If that
assumption is wrong, I think I see your problem. ;-)
-Peter
--
Peter Seibel ·····@javamonkey.com
Lisp is the red pill. -- John Fraser, comp.lang.lisp
Peter Seibel <·····@javamonkey.com> writes:
> I'm not sure I'd give up on the reliable core concept that easy--if
> you've defined a core that you belive covers all the needs of the
> folks who are supposed to be using, it ought to be fairly
> straightforwerd (either by automation or simply by good practice) to
> make sure that no one is using the primitives outside the core.
We have a similar situation here, albeit with a large embedded C++
project. Our "reliable core" is a framework that coordinates several
threads handling network I/O and timers, synchronizing these services
so that the application riding atop can be written in single-threaded,
event-driven fashion. The application code is never called from more
than one "framework thread" at a time; the application can't tell that
there is more than one thread running underneath the main framework
callback loop.
With that in hand, you can have tons of novice-to-intermediate
programmers writing simple application code without having to be
well-versed in concurrent programming. We have these programmers, and
it's almost working out, if only the applications were that simple.
It turns out that most of the applications -- all supposedly
event-driven -- have requirements that prevent them from working well
in (apparently) single-threaded fashion. No callback function can take
too long, for it's holding up the main event loop. So long-running
computations must be haphazardly chopped up into pieces, dispatched by
timers and state machines. The framework can't block on arbitrary
events, so an application-level network connection can't be connected
in and dispatched by the main event loop.� Sometimes this manual
time-slicing, limited to non-blocking operations, is more cumbersome
than just dedicating a worker thread to a given computation and
confronting the synchronization and data sharing details.
Even though the framework is supposed to free the applications from
concurrency constructs, many of the applications can't be written well
without creating extra threads, so we have our under-trained or
inexperienced programmers doing one of two things: writing clumsy,
manually time-sliced, faked-up concurrent programs within the
single-threaded confines of the framework, or stepping outside and
making dangerous concurrency mistakes above the "safe" framework.
We can't win enforcing use of a solution simpler than the actual
problem it aspires to solve.
Footnotes:
� The ACE library's Reactor facility solves these problems. We use it
in places at the application layer because the framework does not
incorporate application-supplied handles for demultiplexing.
--
Steven E. Harris :: ········@raytheon.com
Raytheon :: http://www.raytheon.com
"Steven E. Harris" <········@raytheon.com> writes:
> Peter Seibel <·····@javamonkey.com> writes:
>
> > I'm not sure I'd give up on the reliable core concept that easy--if
> > you've defined a core that you belive covers all the needs of the
> > folks who are supposed to be using, it ought to be fairly
> > straightforwerd (either by automation or simply by good practice) to
> > make sure that no one is using the primitives outside the core.
>
> We have a similar situation here, albeit with a large embedded C++
> project. Our "reliable core" is a framework that coordinates several
> threads handling network I/O and timers, synchronizing these
> services so that the application riding atop can be written in
> single-threaded, event-driven fashion. The application code is never
> called from more than one "framework thread" at a time; the
> application can't tell that there is more than one thread running
> underneath the main framework callback loop.
>
> With that in hand, you can have tons of novice-to-intermediate
> programmers writing simple application code without having to be
> well-versed in concurrent programming. We have these programmers,
> and it's almost working out, if only the applications were that
> simple.
>
> It turns out that most of the applications -- all supposedly
> event-driven -- have requirements that prevent them from working
> well in (apparently) single-threaded fashion. No callback function
> can take too long, for it's holding up the main event loop. So
> long-running computations must be haphazardly chopped up into
> pieces, dispatched by timers and state machines. The framework can't
> block on arbitrary events, so an application-level network
> connection can't be connected in and dispatched by the main event
> loop.� Sometimes this manual time-slicing, limited to non-blocking
> operations, is more cumbersome than just dedicating a worker thread
> to a given computation and confronting the synchronization and data
> sharing details.
>
> Even though the framework is supposed to free the applications from
> concurrency constructs, many of the applications can't be written
> well without creating extra threads, so we have our under-trained or
> inexperienced programmers doing one of two things: writing clumsy,
> manually time-sliced, faked-up concurrent programs within the
> single-threaded confines of the framework, or stepping outside and
> making dangerous concurrency mistakes above the "safe" framework.
Yeah. Been there. Though it has been my experience that when I've had
these kinds of tensions its been because my framework wasn't quite
abstracting things right. Every time I thought really hard about why
we were needing to spin up new threads I'd find some way to both
remove that need *and* simplify the underlying framework. But it
always entailed a lot just banging my head against the problem before
exactly how became clear.
> We can't win enforcing use of a solution simpler than the actual
> problem it aspires to solve.
Yup. But the magical thing (again, in my experience) is that there may
be a way to make the framework conceptually *simpler* yet more capable
of supporting the higher-level needs. Of course figuring out, exactly
what that magical simplification may be can take quite some time--the
last project I worked on that had these kinds of problems started out
as a mess of ad-hoc (and we thought clever) multi-threaded code. Then
we realized it was a mess and got a glimmer of an idea how to
straighten it out. Two and a half years later we had figured out how
to actually consistently apply our insight in most cases.
Writing correct concurrent code is, as you know, hard--the only
approach that seems to work at all is to relentlessly and consistently
apply a very small number of powerful concepts (such as monitors and
condition variables). Whenever I find myself thinking that I have to
do something outside my basic conceptual framework I know I'm about to
sign up for an endless amount of pain that will only end when I figure
out how what I really want to do actually *does* fit into my simple
framework. Which usually entails improving my understanding of both
what I really want to do and my conceputal framework.
-Peter
--
Peter Seibel ·····@javamonkey.com
Lisp is the red pill. -- John Fraser, comp.lang.lisp
Peter Seibel <·····@javamonkey.com> writes:
[bad wait code in Java]
> public synchronized void wait_for_event() {
> try { wait(); } catch(InterruptedException e) {}
> }
[good wait code in Java]
> public synchronized void wait_for_event() {
> int oldCount = count;
> while (count == oldCount) {
> try { wait(); } catch(InterruptedException e) {}
> }
> }
> I noticed this immediately because I've written that pattern out about
> a zillion times since Java doesn't have actual condition variables and
> there's no way to build a condition variable object unless you also
> build your own lock object since you don't quite have sufficient
> control over the built in monitor locks. (And you don't want to build
> your own locks because without macros there's no way to provide a
> syntax that guarantees that you always unlock your locks at the end of
> blocks the way synchronized blocks do.)
I disagree. See below. Yes, macros would make thing better, and the Java
syntax can make things clumsy, but it's not atrocious.
> So back when I used to write multithreaded Java code for a living I
> wished that I was using Lisp because then I could write a macro to
> turn something like:
>
> (wait-for-condition (/= count old-count) lock)
Consider:
abstract public class WaitForCondition
{
abstract public boolean condition();
final public void wait(Object lock)
{
synchronized (lock)
{
while (!condition())
{
try { wait(); } catch(InterruptedException e) {}
}
}
}
}
Then you can do thinks like:
class Event
{
int count = 0;
public void wait_for_event()
{
final int oldCount = count;
WaitForCondition waiter = new WaitForCondition()
{
public boolean condition()
{
return count != oldCount;
}
};
waiter.wait(this);
}
public synchronized void signal_event()
{
count = (count + 1) % 3;
notifyAll();
}
}
--
Cheers, The Rhythm is around me,
The Rhythm has control.
Ray Blaak The Rhythm is inside me,
········@STRIPCAPStelus.net The Rhythm has my soul.
Ray Blaak <········@STRIPCAPStelus.net> writes:
> Peter Seibel <·····@javamonkey.com> writes:
> [bad wait code in Java]
> > public synchronized void wait_for_event() {
> > try { wait(); } catch(InterruptedException e) {}
> > }
>
> [good wait code in Java]
> > public synchronized void wait_for_event() {
> > int oldCount = count;
> > while (count == oldCount) {
> > try { wait(); } catch(InterruptedException e) {}
> > }
> > }
>
> > I noticed this immediately because I've written that pattern out about
> > a zillion times since Java doesn't have actual condition variables and
> > there's no way to build a condition variable object unless you also
> > build your own lock object since you don't quite have sufficient
> > control over the built in monitor locks. (And you don't want to build
> > your own locks because without macros there's no way to provide a
> > syntax that guarantees that you always unlock your locks at the end of
> > blocks the way synchronized blocks do.)
>
> I disagree. See below. Yes, macros would make thing better, and the Java
> syntax can make things clumsy, but it's not atrocious.
>
> > So back when I used to write multithreaded Java code for a living I
> > wished that I was using Lisp because then I could write a macro to
> > turn something like:
> >
> > (wait-for-condition (/= count old-count) lock)
>
> Consider:
>
> abstract public class WaitForCondition
> {
> abstract public boolean condition();
>
> final public void wait(Object lock)
> {
> synchronized (lock)
> {
> while (!condition())
> {
> try { wait(); } catch(InterruptedException e) {}
> }
> }
> }
> }
That's not quite right; you need to change `wait()' to `lock.wait()';
otherwise it will throw an IllegalMonitorStateException (or release
the wrong lock if somehow you've also synchronized on the
WaitForCondition object.) And change the method name wait() to await()
or something, to avoid the clash with the final method on Object.
Then it will work but given that the instantiation of the inner class
has to be inline in order to have access to local variables and that
those variables thus have to be declared final I'm not sure much has
been won. It's not clear to me that this:
public void wait_for_event()
{
final int oldCount = count;
WaitForCondition waiter = new WaitForCondition()
{
public boolean condition()
{
return count != oldCount;
}
};
waiter.wait(this);
}
is a win compared to the straight-forward version:
public synchronized void wait_for_event ()
{
int oldCount = count;
while (count == oldCount)
{
try { wait(); } catch (InterruptedException ie) {}
}
}
That is, by writing a method like wait_for_event() I've already
abstracted it as much as I can. Adding a class that requires more
lines to instantiate than I'm saving isn't a win in my book.
-Peter
--
Peter Seibel ·····@javamonkey.com
Lisp is the red pill. -- John Fraser, comp.lang.lisp
Peter Seibel <·····@javamonkey.com> writes:
> Then it will work but given that the instantiation of the inner class
> has to be inline in order to have access to local variables and that
> those variables thus have to be declared final I'm not sure much has
> been won.
Thanks for the fixes.
The win is is not the avoidance of tedium, which is similar in either
case. The win is that an object like WaitForCondition forces things to be done
(more) correctly, which is the point. That is, it is that much more difficult
to introduce the subtle concurrency errors.
Macros will still be better though, for then you can avoid the tedium as well.
--
Cheers, The Rhythm is around me,
The Rhythm has control.
Ray Blaak The Rhythm is inside me,
········@STRIPCAPStelus.net The Rhythm has my soul.
From: Steven E. Harris
Subject: Re: Why I don't believe in static typing
Date:
Message-ID: <q67wu9xpktn.fsf@raytheon.com>
···@jpl.nasa.gov (Erann Gat) writes:
> Ironically, I actually agree with this.
Can you elaborate? How do types interact with timing conditions?
--
Steven E. Harris :: ········@raytheon.com
Raytheon :: http://www.raytheon.com
From: Steven E. Harris
Subject: Re: Why I don't believe in static typing
Date:
Message-ID: <q67smklpjcg.fsf@raytheon.com>
"Steven E. Harris" <········@raytheon.com> writes:
> How do types interact with timing conditions?
I misread "static /analysis/" and thought you were referring only to
static type checking.
--
Steven E. Harris :: ········@raytheon.com
Raytheon :: http://www.raytheon.com
In article <···············@raytheon.com>, "Steven E. Harris"
<········@raytheon.com> wrote:
> ···@jpl.nasa.gov (Erann Gat) writes:
>
> > Ironically, I actually agree with this.
>
> Can you elaborate? How do types interact with timing conditions?
Static analysis can be used to detect race conditions and other
multi-threading bugs like potential deadlocks. It's not exactly static
typing, but the techniques are similar. And unlike static typing, the
typical mode in which these techniques are deployed is as an adjunct to a
programming language, not as built-in parts of programming languages which
refuse to run your code until you pass all their tests.
This isn't ideal either IMO, because you have to jump through all sorts of
hoops to get your code in a form where the tool can deal with it. The
ideal solution IMO would be to have tools like this -- static analysis for
multithreading bugs, type bugs, etc. -- built-in but optional.
E.
In article <················@tfb.com>, ····@acm.org wrote:
> Erann Gat wrote:
> > And unlike static typing, the typical mode in which these
> > techniques are deployed is as an adjunct to a programming
> > language, not as built-in parts of programming languages
> > which refuse to run your code until you pass all their tests.
>
> So your language of choice requires nothing of what you type in?
Pretty much. My language of choice is Common Lisp, and its surface syntax
is infinitely malleable.
> What
> if your cat runs across the keyboard? Will that necessarily produce
> runnable code?
Of course not. Don't be ridiculous.
> Personally, I can see the value in both approaches. Which means that I
> agree with your calm, deliberative opinion that static typing is not the
> ultimate good, while I disagree with your hysterical opinion that it is
> necessarily bad.
I never said (and don't believe) that static typing is bad. I said that
focusing too much on static typing to the exclusion of other
considerations was bad, and that designing languages with enforced static
typing tends to encourage what I believe to be undue emphasis on static
typing, and that's bad too.
E.
In article <················@tfb.com>, Ken Rose <·······@tfb.com>
wrote:
> What
> if your cat runs across the keyboard? Will that necessarily produce
> runnable code?
The secret is out, Erann! He knows how you code now.
Yes, that's why lispers are so productive - we can get lots of good lisp
programmers, since we're only paying them a can of Friskies a day.
It's finding people who can debug their code that's the problem...
;^)
In article <······································@netnews.attbi.com>,
Raffael Cavallaro <················@junk.mail.me.not.mac.com> wrote:
> In article <················@tfb.com>, Ken Rose <·······@tfb.com>
> wrote:
>
> > What
> > if your cat runs across the keyboard? Will that necessarily produce
> > runnable code?
>
> The secret is out, Erann! He knows how you code now.
>
> Yes, that's why lispers are so productive - we can get lots of good lisp
> programmers, since we're only paying them a can of Friskies a day.
>
> It's finding people who can debug their code that's the problem...
> ;^)
People? I thought that's what our iguanas were for.
E.
Ken Rose wrote:
> The only solid argument I've seen that static typing is significantly in
> the way came from one of the static typers (Was it Joachim?), who
> pointed out that it can sometimes take an annoyingly long time to finish
> propagating a change.
That was me.
Ironically, it was about traditional typing (i.e. the Java way with type
annotations all the way down that a piece of data may take). With type
inference, this effort will be reduced significantly.
Regards,
Jo