The SafeComp 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 instance of safe generation: the guarantee that programs composed from feature modules are type-safe: i.e., 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 references. Safe composition failure can show either an error in the feature 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 feature model.

A feature model of a product-line is specified using the guidsl tool and language. Consequently, errors in such a model may be relatively easily identified through manual inspection. On the other hand, it is far more difficult to keep the implementation aligned with a feature 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 safecomp tool was created in response for automated tool support to ensure safe composition of product-lines.  It reports any implementation level dependencies between features that may not be satisfied under a particular composition of features.

•  Overview
• PLM File Format
• Bytecode Compilation
• Command-Line Invocation
•  Failure Details
• Caveat
  

Overview

This standalone version of safecomp 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:

1. Write the product-line model file (model.m) such that terminals in the grammar refer to feature directories
2. Generate feature directory structure (Foo/*) whose subdirectories are base programs or features
3. Compile all features into class files  (see below how to do this).
4. Run > safecomp Foo model.m

The following general properties are checked by safecomp:

1. Refinements of a class must follow (come after) the 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.
2. 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.
3. 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.
4. Refinements can add an Interface 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 (under revision)

Note: PLM files are only for multi-dimensional models (MDMs) aka “origami”. 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 an n-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 specifies the path to the project root directory. The layer (feature) names are appended to this path. The second section defines the axis and units along each axis. Each unit is separated by a 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"

 

Bytecode Compilation

The safecomp tool requires references from the bytecode to verify compilation dependencies. safecomp requires the following procedure to convert individual jak files within layers (features) into java, and the bytecodes.  Here is the procedure, which must be run under bash. Let Foo be the directory of feature modules (i.e., its subdirectories are base programs and features, and that it has a model.m file):

rem RUN UNDER BASH!

cd to the parent of GPL directory

rm -r Foo\$\$

bcj2j Foo

bccompiler Foo

This procedure will produce "Foo$$" directory containing all layers and class files representing jak source within each layer. For more information on using bytecode compilation tools look into ByteCodeTools in AHEAD documentation.

Note: when bccompiler runs, it will compile all features.  Do not be surprised to get warnings like "using deprecated interface" during compilation.  It is only when files do not compile and real errors are generated will a real problem exist.

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

• 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. mixin and jampack 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 Foo model.m

where Foo is the name of the feature source directory, Foo$$ is the name of the generated directory (see previous section) and model.m is the guidsl model.

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 No Output Failure Details  (default is to print failure details)

      -s No Report Validation Statistics (default is to report validation statistics)

      -d Debugging information - Constraint and Assignment for Failures

      -ie Treat Introduction Constraints as Error (default)

      -iw Treat Introduction Constraints as Warning

      -ii Ignore Introduction Constraints

Failure Details

Isafecomp outputs 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 cannot 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 configurations 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 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 at least 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 a safecomp 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 products in a product-line that can be generated) and safecomp 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 cannot answer the question: If F is selected will G always be selected?

ATS Home Page

Copyright © Software Systems Generator Research Group. All rights reserved.
Revised:  July 07, 2008.