Light Formal Methods in GDB

Light Formal Methods in GDB

[Rob Quill]

Hi,

What I am aiming to do is allow the programmer to debug his program
using linear temporal logic formulas to verify sections of code and
check that specified properties hold.

I consider this important to be included in a debugger as it allows
the programmer to stop the program execution at a certain point, and
check at run-time that parts (or all) of the program are formally
correct.

An example would be the Until operator, which allows the programmer to
specify that expression A must be true until expression B is true.

I know this is a brief explanation, and if it unclear please feel free
to ask me more about it, but I just wanted to see what people think of
the idea.

Thanks,
Rob

Re: Light Formal Methods in GDB

[Michael Snyder]

On Thu, 2006-10-12 at 15:07 +0100, Rob Quill wrote:
> Hi,
> 
> What I am aiming to do is allow the programmer to debug his program
> using linear temporal logic formulas to verify sections of code and
> check that specified properties hold.
> 
> I consider this important to be included in a debugger as it allows
> the programmer to stop the program execution at a certain point, and
> check at run-time that parts (or all) of the program are formally
> correct.
> 
> An example would be the Until operator, which allows the programmer to
> specify that expression A must be true until expression B is true.
> 
> I know this is a brief explanation, and if it unclear please feel free
> to ask me more about it, but I just wanted to see what people think of
> the idea.

Well, gdb can answer questions such as "is expression A true?", 
but only in the context of a specific, static point in the 
execution.  And gdb doesn't know anything about formal or temporal
logic.  Those are way outside its scope.

Are you thinking in terms of, say, a pre-processor that could
come up with a set of properties or propositions, translate them
into language that gdb can understand (eg. "stop here, and see if
expression A is true"), write the results to a file, and then
have a post-processor go over the results and test them against
the logical propositions?

Re: Light Formal Methods in GDB

[Rob Quill]

Hi,

The principle works as follows:

It it possible to create an automaton from an LTL formula, with
expressions for values of variables as the transitions from one state
to the next.

Then the tricky part is building an automaton which represents the
program. But once you have these it is possible to see if the
automaton 'match' and if they do then the property holds.

With regards to building the system automaton, at the very simplest
you could single step the code, get values of variables at each step
and make an appropriate transition on the automaton. However, this is
obviously very inefficient, and improvements would most likely be made
by building a control flow graph of the program (in some way) and use
the nodes of that graph as the points get get values, or something
like that.

The advantage of including something like this in GDB is that once the
property that the programmer expected to hold becomes false, program
execution can stop and he programmer can use the standard GDB tools.
Well, that'd be the idea anyway.

The original idea was to do the same thing but for concurrent programs
because there is research which says that using LTL formulas and the
automaton technique, you can say whether properties of concurrent
programs hold for all the possible interleavings. However, it was
decided that that was too complicated, so it was narrowed to
non-concurrent programs.

Rob

On 12/10/06, Michael Snyder <Michael.Snyder@palmsource.com> wrote:
> On Thu, 2006-10-12 at 15:07 +0100, Rob Quill wrote:
> > Hi,
> >
> > What I am aiming to do is allow the programmer to debug his program
> > using linear temporal logic formulas to verify sections of code and
> > check that specified properties hold.
> >
> > I consider this important to be included in a debugger as it allows
> > the programmer to stop the program execution at a certain point, and
> > check at run-time that parts (or all) of the program are formally
> > correct.
> >
> > An example would be the Until operator, which allows the programmer to
> > specify that expression A must be true until expression B is true.
> >
> > I know this is a brief explanation, and if it unclear please feel free
> > to ask me more about it, but I just wanted to see what people think of
> > the idea.
>
> Well, gdb can answer questions such as "is expression A true?",
> but only in the context of a specific, static point in the
> execution.  And gdb doesn't know anything about formal or temporal
> logic.  Those are way outside its scope.
>
> Are you thinking in terms of, say, a pre-processor that could
> come up with a set of properties or propositions, translate them
> into language that gdb can understand (eg. "stop here, and see if
> expression A is true"), write the results to a file, and then
> have a post-processor go over the results and test them against
> the logical propositions?
>
>
>

Re: Light Formal Methods in GDB

[Michael Snyder]

On Fri, 2006-10-13 at 11:04 +0100, Rob Quill wrote:
> Hi,
> 
> The principle works as follows:
> 
> It it possible to create an automaton from an LTL formula, with
> expressions for values of variables as the transitions from one state
> to the next.
> 
> Then the tricky part is building an automaton which represents the
> program. But once you have these it is possible to see if the
> automaton 'match' and if they do then the property holds.
> 
> With regards to building the system automaton, at the very simplest
> you could single step the code, get values of variables at each step
> and make an appropriate transition on the automaton. However, this is
> obviously very inefficient, and improvements would most likely be made
> by building a control flow graph of the program (in some way) and use
> the nodes of that graph as the points get get values, or something
> like that.
> 
> The advantage of including something like this in GDB is that once the
> property that the programmer expected to hold becomes false, program
> execution can stop and he programmer can use the standard GDB tools.
> Well, that'd be the idea anyway.
> 
> The original idea was to do the same thing but for concurrent programs
> because there is research which says that using LTL formulas and the
> automaton technique, you can say whether properties of concurrent
> programs hold for all the possible interleavings. However, it was
> decided that that was too complicated, so it was narrowed to
> non-concurrent programs.

OK.  Well, once you have your list of nodes and properties (values), 
maybe you could have your software emit a set of breakpoint definitions
for gdb, with appropriate rules for evaluating sets of values at each
breakpoint.  Gdb already has a scripting language that includes "if"
and "while", and you can define debugger-local variables to define
your finite automaton and control its state.  Then, depending on those
state variables, gdb can stop the program or let it continue.  You
can also include "print" statements to log your state.

This sounds like an interesting project, and I don't think 
it should require any modifications to gdb (or at least, any
major ones).  You would generate a script for gdb to set up 
the breakpoints and states, then run gdb in batch mode with
the output piped into a file.  You would then post-process
that file for your results.

Re: Light Formal Methods in GDB

[Rob Quill]

On 13/10/06, Michael Snyder <Michael.Snyder@palmsource.com> wrote:
> On Fri, 2006-10-13 at 11:04 +0100, Rob Quill wrote:
> > Hi,
> >
> > The principle works as follows:
> >
> > It it possible to create an automaton from an LTL formula, with
> > expressions for values of variables as the transitions from one state
> > to the next.
> >
> > Then the tricky part is building an automaton which represents the
> > program. But once you have these it is possible to see if the
> > automaton 'match' and if they do then the property holds.
> >
> > With regards to building the system automaton, at the very simplest
> > you could single step the code, get values of variables at each step
> > and make an appropriate transition on the automaton. However, this is
> > obviously very inefficient, and improvements would most likely be made
> > by building a control flow graph of the program (in some way) and use
> > the nodes of that graph as the points get get values, or something
> > like that.
> >
> > The advantage of including something like this in GDB is that once the
> > property that the programmer expected to hold becomes false, program
> > execution can stop and he programmer can use the standard GDB tools.
> > Well, that'd be the idea anyway.
> >
> > The original idea was to do the same thing but for concurrent programs
> > because there is research which says that using LTL formulas and the
> > automaton technique, you can say whether properties of concurrent
> > programs hold for all the possible interleavings. However, it was
> > decided that that was too complicated, so it was narrowed to
> > non-concurrent programs.
>
> OK.  Well, once you have your list of nodes and properties (values),
> maybe you could have your software emit a set of breakpoint definitions
> for gdb, with appropriate rules for evaluating sets of values at each
> breakpoint.  Gdb already has a scripting language that includes "if"
> and "while", and you can define debugger-local variables to define
> your finite automaton and control its state.  Then, depending on those
> state variables, gdb can stop the program or let it continue.  You
> can also include "print" statements to log your state.
>
> This sounds like an interesting project, and I don't think
> it should require any modifications to gdb (or at least, any
> major ones).  You would generate a script for gdb to set up
> the breakpoints and states, then run gdb in batch mode with
> the output piped into a file.  You would then post-process
> that file for your results.

Hi.

Could you elaborate on this please. I am confused as to how I could
use the GDB scripting language. Can I say things such as "if val = 1"
then do some transition of the automaton and then single step the
program? Or, say that I has somehow already figured out where I wanted
the breakpoints to be I could just set GDB to break there, make
automaton transitions and then keep going.

Is that what you meant? Because that sounds excellent and a lot
simpler than trying to build it into GDB some how, which was what I
thought I would have to do.

Rob

Re: Light Formal Methods in GDB

[Daniel Jacobowitz]

On Mon, Oct 16, 2006 at 11:18:45AM +0100, Rob Quill wrote:
> Hi.
> 
> Could you elaborate on this please. I am confused as to how I could
> use the GDB scripting language. Can I say things such as "if val = 1"
> then do some transition of the automaton and then single step the
> program? Or, say that I has somehow already figured out where I wanted
> the breakpoints to be I could just set GDB to break there, make
> automaton transitions and then keep going.
> 
> Is that what you meant? Because that sounds excellent and a lot
> simpler than trying to build it into GDB some how, which was what I
> thought I would have to do.

I doubt that you could do it directly in GDB's scripting language;
although, it might be possible, with use of the "shell" builtin command
(to run another program to cause the automaton to transform).

However, it sounds to me like what you really want is an external
program in control of GDB.  The only tricky part would be "handing
off" to the user once you've reached a state where the constraints
are violated, but I'm sure that you can find a way to do that.

The external program can initially drive GDB through the MI interface,
then switch interpreters to the CLI for the user.

-- 
Daniel Jacobowitz
CodeSourcery

Re: Light Formal Methods in GDB

[Michael Snyder]

On Mon, 2006-10-16 at 11:18 +0100, Rob Quill wrote:
> On 13/10/06, Michael Snyder <Michael.Snyder@palmsource.com> wrote:

> >
> > OK.  Well, once you have your list of nodes and properties (values),
> > maybe you could have your software emit a set of breakpoint definitions
> > for gdb, with appropriate rules for evaluating sets of values at each
> > breakpoint.  Gdb already has a scripting language that includes "if"
> > and "while", and you can define debugger-local variables to define
> > your finite automaton and control its state.  Then, depending on those
> > state variables, gdb can stop the program or let it continue.  You
> > can also include "print" statements to log your state.
> >
> > This sounds like an interesting project, and I don't think
> > it should require any modifications to gdb (or at least, any
> > major ones).  You would generate a script for gdb to set up
> > the breakpoints and states, then run gdb in batch mode with
> > the output piped into a file.  You would then post-process
> > that file for your results.
> 
> Could you elaborate on this please. I am confused as to how I could
> use the GDB scripting language. Can I say things such as "if val = 1"
> then do some transition of the automaton and then single step the
> program? Or, say that I has somehow already figured out where I wanted
> the breakpoints to be I could just set GDB to break there, make
> automaton transitions and then keep going.

Sure.  First compose all the rules for your automaton.
Then you can compose a gdb script file that might look, 
in part, something like this:

# Create automaton using GDB user-defined variables

set $automaton_state = 0
set $automaton_value1 = 17
set $automaton_value2 = 44
# etc.

# Set up breakpoints to manage state transitions

break foo
commands
  silent
  if (program_var1 > program_var2) && (program_var3 == 0)
    set $automaton_state = 22
  end
end

Consult the gdb docs and runtime help to learn about the
macro command language.


> Is that what you meant? Because that sounds excellent and a lot
> simpler than trying to build it into GDB some how, which was what I
> thought I would have to do.

Yep!