The drc Tool

Not all combinations of AHEAD constants and functions are semantically correct. Selecting a feature may enable the selection of some features; and may disable the selection of others. Design rule checking (DRC) is the counterpart of type-checking in the AHEAD universe. There is a special domain-specific language by which composition constraints of layers are declared. drc is the tool that composes these specifications and notifies users of composition errors. This document describes the process of design rule checking and how it differs from normal type-checking. Also covered are the syntax and semantics of DRC specifications, a discussion of the drc tool itself, and a simple methodology for creating design rules.

Command-Line Invocation

drc is invoked by its name. Its options are listed if no arguments are given:

> drc

Error: Must specify at least one .drc file

Usage: java drc.Main [options] baseFile extensionFile1 extensionFile2 ...
         -f <filename> name of file to generate
         -a <layerName> name of layer to generate
         -s dump symbol table
         -i do nothing option
         -e send error messages to System.out

As an example, the composition of files one.drc and two.drc to produce layer one_two is written as:

drc -a one_two one.drc two.drc

Background

Normal type checking, as found in Java, C++, etc., is insufficient for composing refinements. Type checking is essentially syntax checking; it does not catch deep semantic composition violations. Here's the basic idea. Assume that AHEAD constant and functions are typed. The set of all constants and functions that return the same type is a realm. Realms A and B are listed below. Realm A has two constants and one function; realm B has two functions:

Just from this specification alone, it would seem that any possible type-correct expression is legal. (It would be in Java and C++). However, in general, only selected compositions (e.g., ones that have only one instance of function i, for example) may be legal. To see what is needed, we can equate the above to a grammar:

Every sentence of the above grammar corresponds to a unique expression. Thus, type-checking corresponds to checking for syntactic correctness. Semantic correctness in grammars is modeled by attribute grammars -- attributes are value annotations and predicates over these annotations determine which syntactically-legal combinations of tokens are semantically correct. Such annotations can propagate values from the inner-most terms of an equation outwards (these are called inherited or flowleft attributes); other annotations can propagate their values from the outer-most terms of an equation inward (these are called synthesized or flowright attributes). Thus, equation validation in AHEAD is driven not by type-checking but by attribute grammars. You'll see these ideas more clearly in the following sections.

DRC Specifications

Every AHEAD constant and function should have a DRC specification file of the following form:

layer foo;

flowright Bool c;
flowleft  Int  d;

requires flowright c;
provides flowleft d >= 10;

(1)

(2)

(3)

Line (1) declares the layer named "foo". Lines (2) declare two attributes, c and d. c is an Bool attribute and d is an Int attribute. The adjectives flowleft and flowright designate the type of attribute -- i.e., "inherited" or "synthesized". Lines (3) define preconditions -- requires -- that must be satisfied during a composition and postconditions -- provides -- whose values are propagated to other terms of a AHEAD expression.

Compositions of DRC specifications yield other DRC specifications of the same form, thus allowing composite constants and functions to have DRC specs that are indistinguishable from their primitive counterparts.

DRC Grammar

Layer Declaration

Optionally, "single" may be used. It is common that AHEAD constants and functions (henceforth called layers) can appear only once in an expression or equation. The single modifier indicates that a unit can appear only once. Similarly, the "constant" option tells DRC that the unit whose design rules are described by this file define a constant, not a function. More on this shortly. Finally, the name of the layer is optional. If it is absent, drc will infer its name from the relative location of the file to the model directory. (drc assumes that it runs in the model directory).

Attribute Declaration

Every attribute that is referenced in a DRC specification must be declared. The syntax is:

An attribute can be declared or be externally referenced. When an attribute is declared, it can be externally referenced by other DRC files. The presence of extern in a declaration means that the attribute is defined in another DRC file; if extern is absent, this DRC file declares the attribute. An attribute can not be defined in multiple DRC files that participate in the same AHEAD equation. It is possible that different layers can declare the same attribute, however, these layers cannot appear in the same equation.

The distinction between flowright and flowleft attributes is essential in design rule checking. Consider the equation A(B(C)) or A ● B ● C in the figure to the right, where ● is the composition operator. The values of flowright attributes propagate right (i.e., from the outermost terms of an equation to the innermost). In contrast, the values of flowleft attributes propagate left (i.e., from the innermost terms of an equation to the outermost). Every attribute must be declared either flowright or flowleft.

There are two data types presently supported by drc: Bool and Int. They are described separately in the following sections. Finally, each attribute must be given a unique name.

Attribute Types

Bool

The simplest and most commonly used attribute type is Bool. Bool (which is short for boolean) is somewhat of a misnomer: a Bool attribute can actually have one of three values: true, false, or undefined. When a Bool attribute is declared, its initial value is undefined. Its value can be changed by a postcondition (discussed later).

Int

Int (which is short for integer) again is somewhat of a misnomer in that an Int attribute can be associated with a single integer value or a range of values. When an Int attribute is declared, its initial value is the range of all integers -- minus infinity to plus infinity. Its value can be changed by a postcondition (discussed later).

The set of predicates that can be used (in combination) with Int attributes are:

Predicate		Semantics
A == v		A equals value v
A >= v		A geq value v
A > v		A gtr value v
A <= v		A leq value v
A < v		A lss value v

Design Rules

Design rules are expressed by flowright and flowleft preconditions and postconditions. When you write an equation A(B(C)) or A ● B ● C, Flowright attribute values are propagated from left-to-right. A requires flowright predicate is a precondition that tests the values of flowright attributes that lie immediately to the left of unit B. A provides flowright is a postcondition that propagates values to the right of unit B.

In contrast, flowleft attribute values are propagated from right-to-left. A requires flowleft predicate is a precondition that tests the values of flowleft attributes that lie immediately to the right of unit B. A provides flowleft predicate is a postcondition that propagates values to the left of unit B.

( requires | provides ) ( flowright | flowleft ) <predicate> ;

where a predicate is a conjunction of primitive predicates. "and" is the conjunction operator.

The drc Tool

Simplification and Validation of Individual Files

drc can perform simple validations and predicate simplifications on individual files. Consider:

layer one;

flowleft Int range;
flowright Int val;

requires flowleft 8 < range and range > 30 and 10 < range;
provides flowright 4 <= val and 4 >= val;

drc validates the specification to make sure, for example, that all attributes are defined and their references are legal (e.g., Bool values cannot be referenced as integer ranges, and flowleft predicates reference only flowleft attributes). drc also simplifies a specification and presents it in a canonical manner. The output of drc for the above file is shown below, where the predicates are simplified.

Composition of Files

drc also composes DRC files. The basic algorithm is simple: the flowright (flowleft) precondition of a composition is the conjunction of the primitive preconditions that cannot be evaluated. The flowright (flowleft) postcondition of a composition is the set of assignments (postconditions) made by each primitive of the composition in the order in which they were composed. Consider layer two:

layer two;

extern flowleft Int range;
extern flowright Int val;

provides flowleft range == 50;
requires flowright val == 4;

The composition of one with two is shown in the left declaration below. Remember that the order in which DRC files are composed matters. Composing two with one (shown in the right declaration below) yields a very different result. Study both to understand these differences and how DRC works.

layer one_two;

flowleft Int range;
flowright Int val;

provides flowleft range == 50;
provides flowright val == 4;

layer two_one;

flowleft Int range;
flowright Int val;

requires flowleft 30 < range;
provides flowleft range == 50;
requires flowright val == 4;
provides flowright val == 4;

In general, drc composes flowright-flowleft requires-provides predicates and merges attribute references eliminating extern declarations when attributes are now defined locally.

Design Methodology

It is not immediately obvious how one creates useful design rules. Fortunately, there are simple guidelines that one can follow. A model architect will know, approximately, the shape or structure of the equations that model users will write. A "shape" takes the form of:

strata_4( strata3( strata2( strata1( strata0 ) ) ) )

where strata0 is a constant and strata_x (x>0) denotes a composition of primitive functions. Further, all functions of strata_(i-1) appear before the functions of strata_i. Consider the following examples.

An Int attribute can delineate the boundaries between strata. Let's define rank to be an flowleft Int attribute. The flowleft postcondition (provides flowleft) for strata0 is rank == 1. An flowleft precondition (requires flowleft) for each strata1 function is rank == 1. The last function in strata1 should set rank == 2 as an flowleft postcondition. An flowleft precondition for each strata2 function is rank == 2, and so on. Thus, once the last AHEAD function in each strata is seen, the value of rank is incremented, and only functions from the next strata can be legally composed.

Next, the composition of functions within an individual strata need to be ordered. This can be accomplished by using Bool attributes. For each AHEAD layer y, use the modelexplorer tool to see which classes that layer refines. Identify the layer -- a.k.a. unit -- from which those classes arise; let x be this layer. (There can be several such layers, but the idea that is described in the next few paragraphs holds). Define a Bool property xPresent which is asserted as an flowleft postcondition for x. An flowleft precondition for y is xPresent. (This means that layer x -- or any layer that serves the same purpose as x -- must appear prior to y -- flowright y -- in an equation. By defining a generic property so that different layers or combination of layers can perform the same layer, you don't have to depend on a the use of a particular layer. (Admittedly, most domains have only one implementation of a feature, so there is often a direct dependence among layers. In the general case, you don't want to have design rules that single out specific layers). By following this strategy, you can define design rules that will appropriately order the layers within a strata.

Most design rules can be specified using flowleft attributes. However, there will always be the need for flowright attributes. For example, one can compose layers in a manner that all layer preconditions are satisfied -- e.g., stack strata1 layers on top of strata0 -- but this doesn't mean that all layers are present in order to build a viable system. In such cases, certain properties (e.g., layers with main methods) must appear in a AHEAD equation. These layers can set an flowright postcondition that is propagated all the way back to strata0. (For example, LocalL in FSATS defines a class with a main method. An flowright Bool attribute, mainPresent, can be asserted as an flowright postcondition. The FsatsL layer can define an flowright precondition that requires mainPresent to be asserted. If this precondition is satisfied, then (presumably) a correct equation has been written provided all other flowleft preconditions have been satisfied.

Another source of DRC attributes is the referencing of libraries, which are added to an equation via a layer. I normally require libraries to be present in an equation before they can be referenced, although this is not absolutely necessary. Because classes in libraries don't refine other classes, they can appear anywhere in an equation, as long as they appear precisely once. Testing for the presence or absence of a library is simple: define an flowright Bool attribute libraryPresent, and assert libraryPresent as a postcondition of the library layer. An flowright precondition of the strata0 layer will require libraryPresent to be asserted. Alternatively, one can use flowright or flowleft attributes to define dependencies among client layers and their layer libraries.

Future Work and Limitations

The drc tool is still in its infancy. The following set of changes will eventually be made:

provides flowright v.orig and v < 40;
That is, if v.orig is 2 < v, the above postcondition would be 2 < v < 40. The modifier ".orig" will be added in the future to reference previous attribute values.

Virtually all DRC predicates are conjunctions. One can imagine that disjunctions will arise.

Predicate		Semantics
A		A is true
!A		A is false
?A		A is unknown

The drc (Design Rule Checking) Tool