caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Fergus Henderson <fjh@cs.mu.OZ.AU>
To: Xavier Leroy <xavier.leroy@inria.fr>
Cc: Yoann Padioleau <Yoann.Padioleau@irisa.fr>, caml-list@inria.fr
Subject: Re: [Caml-list] replay debugger
Date: Tue, 27 Nov 2001 01:51:50 +1100	[thread overview]
Message-ID: <20011127015149.A10358@earth.cs.mu.oz.au> (raw)
In-Reply-To: <20011004143909.A16053@pauillac.inria.fr>

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


  reply	other threads:[~2001-11-26 14:51 UTC|newest]

Thread overview: 11+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2001-10-02 17:53 Yoann Padioleau
2001-10-04 12:39 ` Xavier Leroy
2001-11-26 14:51   ` Fergus Henderson [this message]
2001-11-26 16:14     ` Xavier Leroy
2001-11-26 18:40     ` [Caml-list] Beware of compare (and Ocaml beaten by Java) Mattias Waldau
2001-11-27  9:21       ` Xavier Leroy
2001-11-27  9:41         ` Mattias Waldau
2001-11-30  9:12           ` Pierre Weis
2001-12-03 21:37             ` Chris Hecker
2001-11-27 17:03         ` [Caml-list] bytegen.comp_expr error when doing object copying Neil Inala
2001-11-28 20:15           ` Xavier Leroy

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20011127015149.A10358@earth.cs.mu.oz.au \
    --to=fjh@cs.mu.oz.au \
    --cc=Yoann.Padioleau@irisa.fr \
    --cc=caml-list@inria.fr \
    --cc=xavier.leroy@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).