The Safegen Tool

Safe generation is the goal of synthesizing programs with particular properties. A Safe Generator guarantees these properties for any program that can be synthesized. Safe composition is a particular problem of safe generation: the guarantee that programs composed
from feature modules are absent of references to undefined classes, methods, and variables.

Verifying a product line for safe composition establishes whether it is possible to generate a program, through composition of features, that would fail to compile due to missing dependencies. Safe composition failure can show either an error in the model - that the design permits programs that are not intended to be generated - or it can show an implementation error - that the implementation does not follow architectural level dependency rules implied by the model.

A model of a product-line is specified at a higher level of abstraction and is far easier to design that the low-level implementation. Consequently, errors in the model can be relatively easily identified through manual inspection. On the other hand, it is far more difficult to keep the implementation aligned with the product-line model, especially in an iterative development cycle. The laborious alternative of generating every program of the product line after every implementation iteration is impractical for any non-trivial project.

The safegen tool was created in response for automated tool support to ensure safe generation of product-lines. Currently only safe composition properties are verified.

Safe Composition Validation reports any implementation level dependencies between features that may not be satisfied under a particular composition of features.

The following tool is a stand-alone command line utility for invoking Safe Composition Validator. Programmatic invokation is also possible with some minor modifications (email me).

· Overview

· PLM File Format

· Bytecode Compilation

· Command-Line Invocation

· Failure Details

· Caveat

Overview

This stand alone version of Safe Composition Validator requires the model grammar file (.m) and a compiled directory structure of all layers (compilation instructions). It supports both linear 1-dimensional model as well as multi-dimensional models. Multi-dimensional models are defined in a Product Line Matrix (.plm) file (see below).

The most basic scenario of usage is by designing a linear model:

Write the product-line model file (foo/foo.m) such that terminals in the grammar refer to layer directories
Generate layer directory structure (foo/*)
Implement all layers in foo/*
Compile all layers into class files
Run SafeCompositionValidator on foo.m

Following general properties are ensured:

Refinements of a class must succeed introduction (definition) of the class. This includes check for introduction as well as order. If the class is extended instead of introduced, the parent class's introduction is also checked.
Reference to a field, method, or class (Type declaring fields or input parameters to a method) must ensure that the field/method/class is introduced or inherited under any possible composition of the product-line.
Abstract Classes may be refined to add abstract methods. In any given product all concrete classes of the abstract class must implement all abstract methods introduced in the abstract class.
Refinements can add an Interface Class to a concrete class's implements clause. In any given product line each class implementing an interface must have implemented all interface methods.

PLM File Format

Note: PLM files are only for multi-dimensional models (MDMs). If you have not encountered MDMs you probably only have a linear model. See command line usage options for verifying linear models - you only need the .m model file.

A Product Line Matrix file defines an n-dimensional matrix. It is needed only if dimensional model is being verified for safe composition.

The first line contains path to the model file. If a relative path is used, it must be relative to the SafeCompositionValidator execution directory. The remainder of the file is split into three sections, separated by %%. Comments are denoted by starting a line with '

The first section specified path to the project root directory. This layer names are appended to this path. The second section defines the axis and units along each axis. Each unit is separated by space. The final section defines layers within each cell of the matrix. For example, if it is a 2-dimensional matrix, a line will be of the form: "x-coodinateValue y-coordinateValue : layer1 layer2"

projects\GPL2D.m
' First line should always pointing to the model file

' Path to project root directory
projects\GPL

' Each line represents an axis of the multidimensional cube
' Tokens before : mark the axis name, and tokens after : specify the units along that axis
COLUMN : Base WithDriver
ROW : Directed Undirected Weighted UnWeighted BFS DFS Number Connected StrongC Cycle MSTPrim MSTKruskal Shortest Extra

%%

' This section specifies the cell and layers of the matrix
' Each line represents cell of the cube, and is preceded by its coordinates in n-dimensions
' Tuple-format: axis0 axis1 ... axis(n-1) : layers separated by space

Base Directed : Directed
Base Undirected : Undirected
Base Weighted : Weighted
Base UnWeighted : UnWeighted
Base BFS : BFS
Base DFS : DFS
Base Number : Number
Base Connected : Connected
Base StrongC : StronglyConnected Transpose
Base Cycle : Cycle
Base MSTPrim : MSTPrim
Base MSTKruskal : MSTKruskal
Base Shortest : Shortest

WithDriver Directed : DirectedRun
WithDriver Undirected : UnDirectedRun

WithDriver Number : NumberRun
WithDriver Connected : ConnectedRun

WithDriver Cycle : CycleRun
WithDriver MSTPrim : MSTPrimRun
WithDriver MSTKruskal : MSTKruskalRun
WithDriver Shortest : ShortestRun
WithDriver Extra : Benchmark Prog

Bytecode Compilation

The safegen tool requires references from the bytecode to verify compilation dependencies. There are two ways AHEAD model source can be compiled into a program: 1) compose the jak source, convert it to java, and compile the java classes 2) Convert individual jak files within layers into java, compile the java files into bytecode and compose bytecode. safegen tool requires the later approach.

Example:

cd to the parent of GPL directory

run in bash:

rm -r gpl\$\$

bcj2j gpl

bccompiler gpl

This procedure will produce "gpl$$" directory containing all layers and class files representing jak source within each layer. Use this directory as the Project Root for safegen tool. It needs uncomposed compiled classes. For more information on using bytecode compilation tools look into ByteCodeTools.html in AHEAD documentation.

Note: Some jar files (bcjak2java.jar, bcmixin.jar, bcstubgenerator.jar, bctostub.jar, jrename.jar) needs to be added to the class path (typically in setpath.bat or setpath.sh). If your AHEAD build cant find jrename copy jrename files from lib directory of safegen package to AHEAD's bin and lib directories.

Note: Bytecode compilation can be quite painful at first, so keep the following points in mind:

Scripts used in the command above come with ahead source but not ahead build! You might have to put the following directory in your path ahead\standalone\bcbinScripts or simply copy the scripts in that directory to wherever you are executing from.
bccompiler does not like any directories that are strictly not part of a layer - such as images directory or if you have composed an equation from within the model root directory you might have an extra directory lying around (e.g test/ after composing test.equation)
Each file in every layer must contain all imports that it needs. mixing and jampak won't complain if a layer that is composed earlier introduces the import statements, but bccompiler will. Generally it is a good practice for each layer to be self sufficient, reducing composition dependencies.

Command-Line Invocation

To call safegen from the command line, type:

>./safecomp -f -s -ie "examples/GPL" "examples/GPL.m"

runsafegen.sh script simply sets class paths and invokes SafeCompositionValidator with the input parameters. Usage of SafeCompositionValidator is explained with the following BNF style grammar.

Usage: SafeCompositionValidator LINEAR_OR_DIM
LINEAR_OR_DIM: OPTIONS* rootPath modelFile //linear
           | -md OPTIONS* plmFile        //dimensional
OPTIONS: -f
       | -s
       | -d
       | -ie
       | -iw
       | -ii

Constraint: Choose1(-ie, -iw, -ii)

Explanation of optional flags:

      -f Output Failure Details

      -s Report Validation Statistics

      -d Debugging information - Constraint and Assignment for Failures

      -ie Treat Introduction Constraints as Error

      -iw Treat Introduction Constraints as Warning

      -ii Ignore Introduction Constraints

Example:

   Ensure "guidsl.jar;ClassReader.jar;jdom.jar;sat4j.jar" are in your class path. They hould be in AEAD's lib.

  > safecomp -f -s -ii "path" "path"

Failure Details

If -f flag is provided safegen will output details about each failure it encounters. Each dependency generates a constraint that is tested against the model. If the propositional logic constraint is satisfied by the model a failure is reported as a "Failure Info" block of text. However if a constraint can not be satisfied we know that particular dependency can never be violated within the product line model, and we have proved a theorem that holds for all configuration of the model. Further constraints are checked against known theorems and if a match is found it is classified as a duplicate constraint. Duplicate constraints are aggregated into a single Failure Info block. For example consider one of the the Failure Info blocks reported on GPL2D model.

----------| Failure Info |---------
1. Constraint: (Base and MSTPrim) implies not((WithDriver and Extra))
2. Found Assignment: [1]GPL [2]MainGpl [3]Columns [4]Rows [5]RowDefine [6]Gtp [7]Wgt [9]Alg [10]Extra [20]_MSTPrim [21]MSTPrim [30]_Weighted [31]Weighted [36]_Undirected [37]Undirected [38]DriverProg [40]Base

3. Method Reference Dependency Unsatisfied - Referenced members must be defined
4. Layer: MSTPrim => {Benchmark}
5. * Method: 'void run (Vertex)' in Class:Graph$$ references class Graph$$'s method 'void resumeProfile ()'
6. * Method: 'void run (Vertex)' in Class:Graph$$ references class Graph$$'s method 'void stopProfile ()'
7. [Aggregated 2 failures]
-----------------------------------

If debug flag (-d ) is set the first line will report the constraint that failed. What is generally more interesting is the second line - assignment of the model (i.e. a valid equation ignoring the order) that violates a dependency (also on -d). Details about what caused a particular dependency are presented within lines 3+.

In the example above line 3 tells you which type of constraint dependency was being tested - reference, refinement, introduction, etc.
Line 4 tells you dependencies between layers- this information is generally very helpful in pinpointing the error. A => {B, C} means A depends on definitions that are made in both B and C, hence, A requires atleast B or C.
Line 5 and 6 in the example above explains the dependency - in particular within which method it was generated, and what is it dependant on.
If more than one method generates the same constraint the last line reports how many failures were aggregated.

The example above can be interpreted as follows: Method run(vertex) within class Graph which is present in layer MSTPrim references method stopProfile() within the same class. stopProfile() is defined in Benchmark, and the failure reports that it is possible for a model configuration where MSTPrim is selected, thus referencing stopProfile(), however a definition of stopProfile() is absent. The equation that results in the unsatisfied dependency is the assignment reported in line 2 if -d flag is chosen.

Caveat

A lack of Safe Composition error does not imply that the model is "valid". The worst case would be that the entire model may be unsatisfiable (i.e there are no equations that can be generated) and SafeCompositionValidator will not find any composition errors - because there are no compositions in the first place!

A more realistic scenario would be that the model is invalid with respect to one of the features, say feature F (i.e. constraints are such that F will never appear in an equation). Any compositional dependencies being generated from F (say F depends on feature G) are also invalid - since you can not answer the question: If F is selected will G always be selected?

safegen currently does not support validity tests but a future version will.

ATS Home Page