From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.180.207.44 with SMTP id lt12mr2440474wic.5.1373660092849;
 Fri, 12 Jul 2013 13:14:52 -0700 (PDT)
MIME-Version: 1.0
X-FeedAbuse: http://nntpfeed.proxad.net/abuse.pl feeded by 78.192.65.63
Path: 
 border1.nntp.dca3.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!cw2no16732279wib.0!news-out.google.com!b5ni56201wiz.1!nntp.google.com!proxad.net!feeder1-2.proxad.net!nntpfeed.proxad.net!news.muarf.org!news.ecp.fr!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: The future of Spark . Spark 2014 : a wreckage
Date: Fri, 12 Jul 2013 15:14:49 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <krpo3s$kv1$1@loke.gir.dk>
References: <d84b2eb2-eab3-4dec-917c-0498473c1e93@googlegroups.com>
 <krfb56$332$1@loke.gir.dk>
 <7ebe0439-fa4c-4374-a6c7-365ac78e6e39@googlegroups.com>
 <krkums$ldf$1@loke.gir.dk>
 <a20ef22c-36f0-4c04-8d79-6aaadabb8fa6@googlegroups.com>
 <krngv4$m1g$1@loke.gir.dk> <wcck3kvdfgg.fsf@shell01.TheWorld.com>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: loke.gir.dk 1373660092 21473 69.95.181.76 (12 Jul 2013 20:14:52 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Fri, 12 Jul 2013 20:14:52 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
X-Original-Bytes: 2554
Xref: number.nntp.dca.giganews.com comp.lang.ada:182499
Date: 2013-07-12T15:14:49-05:00
List-Id: <comp.lang.ada>

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wcck3kvdfgg.fsf@shell01.TheWorld.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> I'm pretty amazed to find out that I can't debug concurrent programs,
>> because I've been doing it for decades.
>
> Are you done yet?

I presume this is supposed to be a joke of some kind (but without a 
emoticon, can't be sure), and I'm not sure what the joke is supposed to be, 
either.

So, the serious answer: The servers appear to work properly, without 
deadlocks or other problems. There can't be 100% certainty of that, but 
hardly anyone requires that sort of certainty. I'd like a form of 
correctness-by-construction for concurrent programs, but that appears beyond 
the state of the art. I don't see proof tools adding much in this area, the 
main problem is ensuring that bad things are avoided (about the only place 
that proof might help would be in preventing livelock, but that's way down 
the list of problems).

                       Randy.