2014-12-11

Published on 2014-12-11


Translate Forte to SMV

Cache coherence protocols could be translated to a guarded statements format, on which our Forte semantics model is based. And if we have a Forte model of a cache coherence protocol, it should be easy to be translated to other formats such as SMV in the corresponding syntactic level.

Basics about Forte Model

Our Forte model is based on the following definitions.

lettype varType =
    Global {name::string} |
    Param {name::string} {id::int};

lettype expType =
    Var varType |
    Const int |
    iteForm formula expType expType |
    fun string (expType list)
andlettype formula =
    pred (expType list) |
    eqn {left::expType} {right::expType} |
    neg {form::formula} |
    andList {glist::formula list}  |
    orList  {glist::formula list} |
    implyForm {ant::formula} {cons::formula} |
    forallForm {N::int} {fnForm::int->formula} |
    chaos |
    miracle;

lettype statement =
    assign varType expType |
    parallel (statement list) |
    forallStatement {N::int} {fnForm::int->statement};

lettype rule = guard formula statement;
  • varType: represents variables in a cache coherence protocol, which might be either global or a parameterized one. The parameterized variables is similar to arrays in other languages.
  • expType: represents expressions including only variables and constants. Complex expressions are not supported yet. Besides, iteForm, which is designed for selection expression, is also supported, however, not suggested. So is fun type.
  • formula: represents boolean expressions.
    • eqn: represents equation expression.
    • chaos: represents TRUE.
    • miracle: represents FALSE.
    • neg: represents negation expression.
    • andList: represents logical and expression.
    • orList: represents logical or expression.
    • implyForm: represents implication expression.
    • forallForm: represents for all expression. It is equivalent to a andList expression, because in forallForm, the fnForm is a mapper maps an integer in range 1 to N to a formula, and relation to all these formulae is and.
  • statement: represents a set of assignments.
    • assign: represents an assignment which assigns the expType to the varType.
    • parallel: represents a set of parallel assignments.
    • forallStatement: similar to for clause in other languages, but is parallel.
  • rule: represents a transition rule which has a guarded statements form.

Basics about SMV Model

An SMV Model is organized in a main MODULE, which consists of three part: VAR, ASSIGN, SPEC. That is

MODULE main
VAR
    -- variable definitions --
ASSIGN
    -- initializations and transitions --
SPEC
    -- property specifications --
SPEC
    -- there might be more SPECs --
  • VAR: all variables are defined in here, support boolean (TRUE/FALSE), integer range (1 .. 2 or -2 .. -1), enumeration ({red, black, blue}, NOTE that must in lowwer case) and so on. Variable names could include . and [] such as a.b.c[0]. and a full definition of some variables are as:

    VAR
        a.b.c[0] : 1..2;
        a.b.c[1] : 1..2;
        a.d : {yes, no, unknown};
        a.e : boolean;
  • ASSIGN: include initializations init and transitions next. The initializations are executed the moment the code is ran. All transitions will be execution parallel to enter next state, and check all properties, then continue their next round execution.

    ASSIGN
        init(a.e) := FALSE;
        next(a.e) := TRUE;
        next(a.b.c[0]) :=
            case
                a.e : 1;
                TRUE: 2;
            esac;
  • SPEC: represents property which this SMV code must hold. It is written in CTL formula.

    SPEC
        AF (a.b.c[0] = 1)

Strategy to Translation

As we know, in Forte, all rules, invariants, even variables, could be parameterized. However, SMV is a simple but complete language. So this translation work is not trivial. Obviously, the very first step is to instantiate all parameterized rules, invariants and variables. Then, we need to analyze these elements to extract information needed. Finally, we act the translation.

Instantiate Rules

Parameterized rules are functions in fact, which map the parameters to the corresponding rules. The type of rules is as int -> *a -> *b -> *c -> *d -> rule. In this example, the latter four parameters do not have type int, because this is a rule with one parameter.

To instantiate a rule, we need its parameter information including parameters' count and type. However, even we know these information, it is also difficult to instantiate the rules automatically, because different rules with different count of parameters are of different types, e.g., int -> *a -> *b -> *c -> *d -> rule and int -> *a -> *b -> rule are different types. And once our instantiation function were evaluated to a specific rule type, it could not be called with other types!

In fact, if you think in another way, it will be much more easier to instantiate rules. A Forte program about a cache coherence protocol is written by a user who knows how many parameters there is. So when the user need to translate his code, he should provide the way to instantiate rules, e.i., provide a function maps a parameterized rule and its actual parameter list to a actual rule. For example, to instantiate a 5-parameter rule, provide

let ruleFuncMap rule [a, b, c, d, e] = rule a b c d e;

To generate the actual parameter lists for each parameterized rule, the user should also provide a rule-parameter-type table. For example, suppose there is a rule named Test whose type is int -> *a -> *b -> *c -> *d -> rule:

let NodeType = [1, 2]; // there are two nodes

// the rule-parameter-type table
let paraTypeTable =
    let t = tbl_create 1 in
    // [] represents parameter type of useless parameters
    let t = tbl_insert t "Test" [[NodeType], [], [], [], []] in
    t;

Then what we need is that generate actual parameter lists with the parameter types. For example, provide [[1, 2], [], [], [], []], we produce [1, 0, 0, 0, 0] and [2, 0, 0, 0, 0], which is what we want. This is not a difficult work.

// generate all possible combinations for a specific choice list
// for example, input [[1,2],[1,2],[]] gives [[1,1,0],[1,2,0],[2,1,0],[2,2,0]]
// NOTE that [] will be generated as 0
letrec combinationGen res [] =
        res
    /\ combinationGen [] (p:choice) =
        combinationGen (map (\x. [x]) p) choice
    /\ combinationGen res ([]:choice) =
        combinationGen (map (\x. x@[0]) res) choice
    /\ combinationGen [] ([]:choice) =
        combinationGen [[0]] choice
    /\ combinationGen res (p:choice) =
        let incPara res i = map (\x. x@[i]) res in
        combinationGen (itlist (\x.\r. (incPara res x)@r) p []) choice;
// combinationGen

Instantiate Invariants

Instantiation of invariants is quite similar to the process for rules, even we can use a same map function. However, you must write the map function with another name again, because after evaluation, the function for rules will have type rule, and here it should have type formula.

Instantiate Variables

It's an easy work. For a parameterized variable Param "v" i, just translate to v[i].

Analysis

The goal of analysis is to generate an intermediate result, so that we can act the translation easily.

As we known, the rules have type guard formula statement, and all statements have type or equivalent type parallel ((assign varType expType) list). Our analysis work for rules is to extract informations about each variable. The information contains the variables is modified in which rule, and what value the variable is to be assigned. These informations are stored in a table, with the name of variables as key, and corresponding tupls (associatedGuardFormulae, associatedExpressions) as value. Once this work was done, the actual variables is also ready.

The analysis for initialization is quite similar but a little different, which has the sequence of expType assigned as value.

Translation

The translation is not very difficult. And finally we get a entrance function:

// do translation
let trans2smv fileName typeTab ruleTab paraTypeTab invTab invTypeTab init ruleFuncMap invFuncMap enumValTab dist =
    let file = fopen (fileName^".smv") "w" in
    fputs file "\n-- This program is generated by trans2smv from its forte version. --\n" fseq
    fputs file "\nMODULE main\n" fseq
    fputs file "\nVAR\n" fseq
    fputs file (transVar 1 typeTab ruleTab paraTypeTab ruleFuncMap enumValTab dist) fseq
    fputs file "\nASSIGN\n" fseq
    fputs file (transInit 1 init enumValTab dist) fseq
    fputs file (transNext 1 ruleTab paraTypeTab ruleFuncMap enumValTab dist) fseq
    fputs file (transInv 0 invTab invTypeTab invFuncMap enumValTab dist) fseq
    fclose file;
// trans2smv

Some Tips

About #if

Use #if to ensure that every module of Forte could be loaded only once. The following example is to load createIsaModel0125.fl, but if it was already loaded, we would do nothing.

#if (is_defined "findInvsFromParaRulesByInvs");
    let createIsaModel = ();
#else;
    let createIsaModel = load "creatIsaModel0125.fl";
#endif;
createIsaModel;

In fact, if we write the loaded files carefully, we need not do this everywhere we load it. For example, in trans2smv, we use

#if (NOT (is_defined "trans2smv"));
// code of trans2smv
#endif;

Then we can load trans2smv without do anything, because it would be loaded only once.

About Select Rules Randomly

In Forte, if there are several rules could be executed, a random one will be selected. Unfortunately, after translate to SMV, all the rules whose guards are satisfied will be executed together. This is wrong! So we should simulate the selection in SMV.

After instantiation of rules, we know how many rules here is, then we numbered them, and add a guard condition in the guard part of each rule which requires the current chosen rule is itself so that transition of variables in SMV will be triggered only when the corresponding guard is satisfied and the rule is selected.

In SMV, the selection is simulated by a variable, and we need also define it, initialize it and modify it.