English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
How can I treat bits?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2001-11-26 (14:51)
From: Fergus Henderson <fjh@c...>
Subject: Re: [Caml-list] replay debugger
On 04-Oct-2001, Xavier Leroy <xavier.leroy@inria.fr> wrote:
> [The question was: how does the OCaml debugger implements reverse execution?]
> > Y'a t'il de la doc sur le fonctionnement interne du debuggger.
> > Comment ca marche ? comment ki fait pour revenir en arriere ?
> Like all "time-travel" debuggers: by periodic checkpointing.

I think that comment could be misleading.

According to the Academic Press Dictionary of Science and Technology,
"checkpoint" means

 |      [...] Computer Programming.  A designated point in a program where
 |      processing is interrupted and all status information is recorded
 |      in order to be able to restart the process at that point, thus
 |      avoiding the necessity to repeat the processing from the beginning.

So I think it would be reasonable to interpret Xavier's comment as
meaning that you must periodically save the entire state of the program.

But that's not how logic programming debuggers, such as those for Mercury
and various Prolog implementations, do it.  Rather than periodically
checkpointing the entire state, these systems keep an incremental record
of all destructive updates performed, on a separate stack called the
"trail".  On backtracking, the system will unwind the trail,
restoring all the modified objects to their original values.

Now, this may be a matter of terminology.  I consider "checkpointing"
and "trailing" to be two different ways of achieving the same result
("replay debugging", in this case, or more generally "roll-back capability"). 
But maybe Xavier had in mind a broader definition of "checkpointing",
which would encompass trailing.

> We learnt this trick from Andrew Tolmach's thesis:
>         http://www.cs.pdx.edu/~apt/thesis.ps.Z

Looking at the details here [or at least those which show up on the first
few pages -- after that, ghostview reports a Postscript error :-( ],
it seems that the technique described here is actually much more
similar to typical Prolog implementations than Ocaml's fork()-based
implementation.  In particular, Tolmach uses a "history log", which
sounds like it would be pretty much identical to the Prolog trail,
for recording updates to mutable data structures.

Fergus Henderson <fjh@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.
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr