MAGIC Version 1.0 Tutorial

Table of Contents

A Simple Implementation

The goal of MAGIC is to ascertain that an implementation conforms to a specification. The implementation is always a (possibly concurrent) C program, with each sequential component being a C procedure. Let us begin with a simple sequential implementation.

int my_proc(int x)
{
    int y;
    if(x == 0) {
       y = foo();
       if(y > 0) return 10;
       else return 20;
    } else {
       y = bar();
       if(y < 0) return 30;
       else return 40;
    }
}

Back to Top

A Simple Specification

We shall now try to construct an appropriate specification for my_proc and then verify it. Note that we are intentionally doing this in a roundabout way for ease of understanding. Normally, if standard software engineering practices have been followed, the specification always comes into existence before the implementation.

So what could be a good specification for my_proc? In a kind of pseudo-code, one might make the following claim about my_proc:
  1. If the first argument to my_proc is equal to zero:
    • my_proc calls the library routine foo.
    • Depending on whether the value returned by foo is greater than zero or not, my_proc returns either 10 or 20.
  2. Otherwise, if the first argument to my_proc is not equal to zero:
    • my_proc calls the library routine bar.
    • Depending on whether the value returned by bar is less than zero or not, my_proc returns either 30 or 40.

It is clear that any specification of my_proc must take into account its calling context, since the behavior of my_proc is dependent on the value of its first argument. Further, the behavior of my_proc in the first case (i.e. when its first argument is equal to zero) can be expressed by the following simple state machine.

SPEC-Figure

Back to Top

Writing down LTSs

MAGIC uses an extended FSP notation to specify state machines. The above state machine can be expressed in MAGIC's notation as follows:

S1 = ( call_foo -> S2 ),
S2 = ( return {$0 == 10} -> STOP | return {$0 == 20} -> STOP ).

Note that the name of a state machine is simply the name of its initial state. Also note that the transitions of the state machine are labelled with actions.Such state machines are also known as labelled transition systems (LTSs). The transition from the initial state (S1) is labelled by an action call_foo. This action encapsulates the externally observable event of library routine foo being invoked. Such actions, with only names, are also called basic actions.

Back to Top

Return actions

As anyone familiar with the FSP will realize, we extend the FSP notation to express a special class of actions called return actions. Return actions are of the form return {expression} or return {} where the former expresses the return of an integer value and the latter expresses returning a void value. In a return action of the form return {expression}, the expression represents a condition satisfied by the return value. The return value itself is represented by the dummy variable $0.For instance, the action return {$0 < 5} represents the return of an integer value less than 5.

Note: The notation for return actions in version 1.0 is a major departure from version 0.1. In version 0.1 we could write return {10} to specify the return of 10 but there was no way to specify the return of a value less that 10. In version 1.0 this can be achieved simply by return {$0 < 10}.

Back to Top

Procedure Block

We are now ready to express the fact that S1 specifies the behavior of my_proc when the first argument of my_proc is equal to zero. In MAGIC, this can be achieved by the following procedure block:

cproc my_proc {
        abstract { abs_1 , ($1 == 0) , S1 };
}

Note the keywords cproc and abstract. The block keyword cproc indicates that we are going to say something about a C procedure. It is followed by the name of the procedure and then by a set of statements enclosed within a pair of curly braces. Each such statement typically consists of an statement keyword followed by other terms. The procedure whose name follows cproc is often referred to as the scope procedure.

One such statement keyword is abstract.This keyword indicates that we are expressing an abstraction relation between the scope procedure and an LTS. Note the guard ($1 == 0) where $1 refers to the first argument. In general $i can be used to refer to the i-th argument of the scope procedure. Finally note that the abstraction statement has a name, abs_1. For procedure blocks, the abstraction names are just placeholders and have no special significance.  However, soon we will discuss program blocks and for them, the names of abstraction statements will be of crucial importance.

The following LTS expresses the behavior of my_proc when its first argument is not equal to zero:

S3 = ( call_bar -> S4 ),
S4 = ( return {$0 == 30} -> STOP | return {$0 == 40} -> STOP ).

Thus we can have another procedure block to specify the relation between my_proc and S3.

cproc my_proc {
       abstract { abs_2 , ($1 != 0) , S3 };
}
In general, multiple procedure blocks can be combined into one as long as they have the same scope procedure. Also the order of statements within a procedure block is irrelevant. Thus, the above two procedure blocks together is equivalent to the following single procedure block:

cproc my_proc {
       abstract { abs_2 , ($1 != 0) , S3 };
       abstract { abs_1 , ($1 == 0) , S1 };
}

MAGIC requires that the guards of abstraction statements for any scope procedure be mutually disjoint and complete (i.e. cover all possibilities of argument valuations). This is necessary to enable MAGIC to unambiguously identify the applicable abstraction in any given calling context of the scope procedure.

Back to Top

Specifying Library Routines

In order to construct a proper model for my_proc MAGIC must know about the behavior of the library routines called by my_proc. Let us assume that the actual code for foo and bar are unavailable. In such a case, MAGIC requires that the user supply appropriate abstractions for these two routines. In particular, suppose that foo andbar are respectively abstracted by the LTSs FOO and BAR described below:

FOO = ( call_foo -> return {$0 == -1} -> STOP ).
BAR = ( call_bar -> return {$0 == 50} -> STOP ).

Then the following program blocks can be used to express the relation between foo, bar and their abstractions.

cproc foo {
       abstract { abs_3 , (1) , FOO };
}

cproc bar {
       abstract { abs_4, (1), BAR };
}

Note that the guard in both abstraction statements is 1, which denotes TRUE according to C semantics. This therefore means that under all calling contexts, foo and bar are abstracted by FOO and BAR respectively. Also note that specifications and abstractions are syntactically identical. This makes sense because both abstractions and specifications are essentially asserting the same thing viz. that under a certain calling context, a procedure's behavior is subsumed by the behavior of an LTS. The only difference is that the assertion made by an abstraction can be assumed to be true while the assertion made by a specification needs to be validated. This has at least two significant consequences:
Back to Top

Program Block

It is now time to specify the entire program that we want to verify. In our case the program is sequential, i.e. it has a single component consisting of the procedure my_proc. The following program block expresses the relation between our program and its specification:

cprog my_prog = my_proc {
        abstract abs_5, {($1 == 0)}, S1;
        abstract abs_6, {($1 != 0)}, S3;
}

This looks a lot like a procedure block but there are some crucial differences. First, it begins with the keyword cprog and not cproc. This is followed by the name of the program (which is again a placeholder and does not serve any other purpose), an equal to sign and then a list of procedure names. Intuitively these are the names of the procedures which execute in parallel and constitute the program. In the above block this list has a single procedure name viz. my_proc, signifying that our program has just one component that executes my_proc.

Following the list of procedure names we have a sequence of statements enclosed within curly braces. Just like procedure blocks, abstraction statements are used to provide specifications. But abstraction statements for program blocks are syntactically different. They do begin with the abstract keyword, but the rest of it them is not enclosed within curly braces. Instead there are three components. The first is the name of the abstraction statement. This is used by MAGIC to identify the target abstraction to be validated. The second is a list of guards, one for each component of the program. Each guard in the list expresses the beginning state of the corresponding component. In the above block, the list has just one element that expresses the starting context of my_proc. Note that the list of guards is enclosed within curly braces. The third and final component is the name of the LTS which specifies the program.

Back to Top

Comments

You can use either C-style or C++ style comments in specification files.

/* this is a comment */
// so is this one

 Back to Top

Running MAGIC

We are now ready to try out MAGIC. First save the C program in a file whose name must end with ".pp", say my_proc.pp. Next save the specifications in another file whose name ends with ".spec", for example my_spec-1.0.spec. Finally run MAGIC:

$ magic --abstraction abs_5 my_proc.pp my_spec-1.0.spec --optPred

MAGIC will try to validate the abstraction statement with name abs_5. The --optPred options tells MAGIC to perform counterexample guided abstraction refinement with predicate minimization. It is usually a good idea to always use this option. For details on other options that MAGIC can accept, look at the user's manual. If all goes well, MAGIC should be able to successfully verify the abstraction and produce an output that ends with something like this:

conformance relation exists !!
abstraction abs_5 is valid ...
Simplify process destroyed ...
terminating normally ...

Similarly you can try to verify abs_6and MAGIC should be able to do it. If you look again at my_spec-1.0.spec you will notice that we have added two more abstraction statements, abs_7 and abs_8, to the my_prog block. They are similar to abs_5 and abs_6 except that the guard conditions have been switched. Clearly they are invalid specifications and MAGIC should be able to detect this. Try verifying abs_7 by typing the following:

$ magic --abstraction abs_7 my_proc.pp my_spec-1.0.spec --optPred --ceShowAct

MAGIC should tell you that this is an invalid specification and further provide you with a counterexample. The output should look something like the following:

*******************************************
branch ( P0::x == 0 ) : [P0::x == 0] : TRUE
############ P0::epsilon ############
P0::y = foo (  ) : []
############ P0::epsilon ############
P0::y = foo (  ) : []
############ call_foo ############
P0::y = foo (  ) : []
############ {P0::y = [ -1 ]} ############
branch ( P0::y > 0 ) : [] : TRUE
############ P0::epsilon ############
return ( 10 ) : []
############ return { ! } ############
*******************************************
CE dag projections analysed ...
conformance relation does not exist !!
abstraction abs_7 is invalid ...
Simplify process destroyed ...
terminating normally ...

Back to Top

A Concurrent Example

Let us now verify a concurrent program. Our concurrent program will be very simple. It will be two copies of my_proc executing in parallel. This is easy to understand because the resulting parallel program should behave exactly like a single copy of my_proc  (since our notion of parallel composition is idempotent). All we need to do is create a new program block specifying our example. Here is a sample my_conc-1.0.spec.Notice that it has four abstraction statements abs_9, abs_10, abs_11 and abs_12 out of which the first two are valid while the last two are invalid.We can try to verify abs_9 by the following command:

$ magic --abstraction abs_9 my_proc.pp my_conc-1.0.spec --optPred

This should succeed. Likewise MAGIC should be able to prove that abs_10 is also valid while abs_11 and abs_12 are both invalid.

Back to Top

Other Keywords

In addition to abstract, there are several other keywords that can be used in procedure blocks for performing specific tasks. In this section we mention a few important ones.

Back to Top

Supplying predicates

The user can manually supply predicates to guide MAGIC's predicate abstraction. Often this is useful when MAGIC fails to discover a satisfactory set of predicates in a reasonable amount of time. Predicates are supplied in a per-procedure basis. An important feature of MAGIC is that all user-supplied predicates for a procedure proc must be syntactically equivalent to some branch condition in proc.Otherwise that predicate will be simply ignored by MAGIC. For example consider the following C procedure:

int proc()
{
    int x = 5;
    if(x < 10) return -1;
    else return 0;
}

Suppose we want to prove using MAGIC that proc is correctly specified by the following LTS:

PROC = ( return {$0 == -1} -> STOP ).

Normally we would do this by simply asking MAGIC to perform automated abstraction refinement (using the --optPred option). However suppose we have a good idea about which predicate MAGIC will need to complete successfully. For example, in this case (x < 10) is the required predicate (note that this corresponds to a branch condition in proc). Then we can simply tell MAGIC to use this predicate by using the predicate keyword. The following procedure block shows how to do this:

cproc proc {
       predicate (x < 10);
}

MAGIC will look for branch statements in proc which have a branch condition (x < 10). If it finds any such branch, it will use the corresponding branch condition as a seed predicate. Otherwise it will ignore the user supplied predicate. Multiple predicates can be supplied in one statement using a comma-separated list or they can be supplied via multiple predicate statements. Also the order in which predicates are supplied is irrelevant. For example the two following procedure blocks each have the same effect as the procedure block above:

cproc proc {
       predicate (y == 10) , (w == 5) , (z +w > 20) , (x < 10) , (x+y != 5);
}

cproc proc {
       predicate (x+y != 5);
       predicate (z+w > 20) , (y == 10);
       predicate (x < 10) , (w == 5);
}

Back to Top

Inlining Procedures

Suppose procedure foo calls procedure bar. Normally MAGIC will not inline bar within foo even if the code for bar is available. It has to be told explicitly to do this via the inline keyword. Here's a procedure block that demonstrates how to do this. Once again inlining has to be done on a procedure-to-procedure basis. For example the following procedure block will not cause bar to be inlined within some other procedure baz.

cproc foo {
       inline bar;
}

Back to Top

Drawing with MAGIC

MAGIC can be used to output control flow graphs, LTSs and intermediate data structures as postscript files. This is very useful for visualization and understanding. For example, using the following command line on these draw.pp and draw-1.0.spec files produces this draw-1.0.ps file.

$ magic --abstraction abs_1 draw.pp draw-1.0.spec --optPred --drawPredAbsLTS --drawFile draw-1.0.ps

Also, using the following command line on my_proc.pp and my_spec-1.0.spec yields this my_proc-1.0.ps.

$ magic --abstraction abs_5 my_proc.pp my_spec-1.0.spec --optPred --drawPredAbsLTS --drawFile my_proc-1.0.ps

Please look at the user's manual for more details on command line options that control MAGIC's drawing capabilities. Also note that in order to draw its figures MAGIC requires the Graphviz package, and in particular the DOT tool. However, if you do not want to use MAGIC's drawing capabilities, there is no need to install Graphviz.

Back to Top

Questions and Comments

At this point, you should be more or less familiar with MAGIC. However I am sure there will be many questions and suggestions. Please feel free to email me and I will do my best to respond promptly and correctly. Have fun with MAGIC !!

Back to Top

HOME