[e-lang] Draft "Causeway: A message-oriented distributed debugger" -- please comment

[Toby Murray]

On Thu, 2009-02-19 at 21:24 -0800, Terry Stanley wrote:
> Tyler Close, Mark Miller, and I are writing a paper on Causeway. Our
> current draft is at
> <http://erights.org/elang/tools/causeway/cw-paper09.pdf>.

Awesome. Look forward to reading it.

On related and future work, a few things spring to mind:

1. ProBE

Formal System's (Europe), Limited's ProBE tool for exploring CSP models.
See http://www.fsel.com/probe_download.html which includes downloads and
documentation etc.

Quoting from a synopsis about ProBE:
"ProBE is another offering from Formal Systems. In contrast to FDR's
automatic checking of properties, ProBE addresses the equally important
need of the user to gain understanding of a system by interacting with
it." ... "The user controls the resolution of non-determinism and the
choice of actions, watching the process evolve in response. Component
processes can be selected, and their contribution to the larger system
examined."

ProBE differs from Causeway in that it's not a debugger, but it does
feature a similar treeview-based UI that allows one to do a "follow the
message" view of a system (more precisely a "follow the events" view,
but events usually model messages). ProBE has been around for quite a
while. It was publicly released in 1997, see
http://phase.hpcc.jp/phase/swopp-announce/archives/msg00437.html .


2. The work of Alex Groce

Causeway is focused on helping a programmer understand the "cause" of a
bug, right? It does so by allowing them to examine the trace of events
the led to the bug, presenting the information in such a way to allow
the programmer to more naturally understand what caused the failure.
This process is "manual" in the sense that the programmer must discern
for him/herself what the cause is, using the information that causeway
presents. There has been a bit of work on automating sort of thing,
namely in the automatic analysis of
sequences-of-events-leading-to-failures to determine which events
"caused" the failure in question. A notable example is the PhD thesis of
Alex Groce, see http://www.cs.cmu.edu/~agroce/ . He defines a formal
definition of causation and then applies this to
sequences-of-events-leading-to-failures (in the form of
counter-examples, generated by some model checker that has found a
sequence-of-events after which some correctness condition is violated)
to determine the events that caused the failure.

Adding these sorts of capabilities to causeway would be an ideal thing
to mention for future work IMO.

Cheers

Toby