## 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*.

- eqn: represents
- 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.

- assign: represents an assignment which assigns the
- 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.