The Implementation relation

When types are created using either deftype or defchan, they are defined as the implementation of a type. This is also possible for processes defined using defproc.

The implementation relation is used to specify the precise implementation of a data or channel type. The most straightforward mechanism to specify a channel is to say that it is the implementation of a built-in data type. In the example in the previous section, the channel e1of2 is defined to be an implementation of a chan(bool). The implementation has additional port parameters, and it specifies the communication protocols for a send and receive action. The syntax that is used to say that we have an implementation is the <: symbol between the name of the type and the parent type that it is related to.

When a type implements another one, the new type can be used in places the old type was used. While this is superficially similar to subtyping in programming languages, it is better viewed as an implementation relationship. So, if type tA implements type tB, then tA has a more detailed description of the implementation compared to tB. Type tB is the parent type for type tA. As seen earlier, each data type or channel type can have a method body that specifies all the operations that can be performed using the type. These method bodies relate operations on the type to operations on the parent type (through self).

Different implementations of the same type are not equivalent or interchangeable. For example, one can imagine two different implementations of an int<2>: two dual-rail codes, or a one-of-four code. Both are implementations, but they are not equivalent to each other.

A more interesting option is to use the implementation relationship between two user-defined types. This option is used to create related versions of an existing type. If type foo implements bar, then the basic rule is that one can use foo instances in all the same contexts where bar instances can be used. The meaning of defining one type to be an implementation of another is discussed in detail below.

When a user defined type implements another, there are several items to consider: (i) the template parameters (if any); (ii) the port parameters; and the body of the new type. Since the new type is supposed to implement the old one, ACT defines the template parameters and port parameters for the new type using the old type as a starting point.

The port list of the new type consists of the original port list in the base type plus the additional ports specified in the type definition—in other words, the new type extends the original port list. As an illustration, consider:

defproc type1 (bool a, b) { ... }
defproc type2 <: type1 (bool c) { ... }

In this case type2 would have ports a, b, and c, since it is an implementation of type1.

Template parameters are handled in a similar fashion, except there is a complication. In the example below, type2 would have two template parameters N and M, as might be expected from the port list example above.

template<pint N>
defproc type1 (bool a, b) { ... }
 
template<pint M>
defproc type2 <: type1 (bool c) { ... }

However, we can also define type2 in the following manner:

template<pint N>
defproc type1 (bool a, b) { ... }
 
template<pint M>
defproc type2 <: type1<4> (bool c) { ... }

In this version, the template parameter from type1 has been specified in the type definition for type2. To permit this feature, template parameters for the new type are defined in the following manner:

• Template parameters are categorized as definable parameters versus pre-specified parameters. Fresh template parameters are always definable.
• Pre-specified parameters are not part of the parameter set that can be specified when a type is created.
• The value of the pre-specified parameter is computed based on the type signature.
• The list of parameters accessible in the body of the type and outside the type is the combination of the ones defined by the new type and the parent type.
• The order of template parameters in the new type corresponds to the new parameters first (in the order specified), followed by any definable parameters left in the parent type.

So in the example above, we could create an instance of type2 as follows:

type2<5> x;
// x.N, x.M are both accessible!

The parameter N for x will be 4, since that has been pre-specified in the type definition for type2. If instead we had specified type2 <: type1 as in the earlier example, then the instance

type2<5,7> x;
// x.M=5, x.N=7

would set M (the new template parameter) to 5, and N (the parent, still definable parameter) to 7. Finally, the following would be an error:

template<pint N> defproc type1 (bool a, b) { ... }
template<pint N> defproc type2 <: type1 (bool c) { ... }

-[ERROR]-> Duplicate meta-parameter name in port list: `N'
           Conflict occurs due to parent type: type1

since the name of the template parameter is repeated.

The body of the new type is the union of the original type definition and the new body. As an example to illustrate how this might be used, consider the following example:

defproc buffer (e1of2? l, e1of2! r)
{
   bool x;
 
   chp {
     *[ l?x;r!x ]
   }
}

buffer specifies the CHP description for a one-place FIFO. This can be implemented using a variety of circuits, and hence we could define a specific implementation as follows:

defproc wchb <: buffer ()
{
   prs {
     ...
   }
}

The process wchb is a specific implementation of the buffer (without any extra ports) that contains a particular production-rule implementation of the same buffer.

Consider the buffer example above. A better and more abstract specification for a buffer at the CHP level of abstraction would be:

defproc buffer (chan?(bool) l, chan!(bool) r)
{
   bool x;
 
   chp {
     *[ l?x;r!x ]
   }
}

The production rules for this buffer use the fact that the Boolean channel for l and r is in fact an e1of2 channel. Because an e1of2 channel implements a chan(bool), ACT provides a mechanism to say that an implementation of a process also replaces existing types with new implementations of the same type. This mechanism is called an override, because old types can be overridden with new ones that implement them.

Variables in the port list as well as the body of a type can be overridden. For this to be sound, the new type must be an implementation of the original. The syntax for this is shown below:

defproc wchb <: buffer()
+{ e1of2 l, r; } // override block
{
   prs {
     ...
   }
}

In this version, the original process implements a buffer with channels, and the wchb specifies that the channel is a e1of2. The first abstract buffer can be used with different handshake protocols on channels, or with different circuits.

The +{ … } indicates the override block. The override block uses the instantiation syntax to specify override types. The only syntax permited is of the form within an override block is

+{
    type list-of-ids;
    ...
 }

The identifiers cannot contain array specifiers, and the types cannot have any direction flags. Furthermore, the types must also be user-defined types. The identifier names must match names in the parent type (either in the port list or in the body of the type). If the original identifier was declared as an array, the entire array will be overridden. Direction flags from the parent type will be inherited by the overridden type.

Implementation relations introduced should be handled with care. For example, suppose one has two definitions of a buffer: one using the CHP language, and the other using the PRS language (as above), and consider the variable x. Now this internal variable which is in the CHP language may not be part of the PRS for the WCHB reshuffling. In other words, the wchb process will not have any internal variable that corresponds to x in the CHP language! Similarly, the wchb PRS language will contain additional variables that are not present in the CHP language. The relation between such variables is unspecified by the implementation relationship.

An additional complication arises if the process wchb ends up introducing a state variable x in the PRS language that does correspond to the bool x in the CHP language. In this case, one should override x as well with the appropriate detailed representation of the Boolean variable.

An instance created in a type definition may be created only under certain circumstances. This can occur in templated types, where template parameters can affect the instances within the type. The override block has the simple syntax shown above. However, to account for conditional instances, the override block directives implicitly check if the instance exists before applying the override. (Note that ACT does not permit different types for the same instance name under different conditions.)

When a type is being overridden by another, the new implementation may have additional template parameters. The override syntax above requires the complete list of template parameters to be specified. Instead, we also provide a single extension override syntax

+{
    type<param>+ id;   // single ID only
    ...
 }

The + indicates that this is an extra template parameter that should be added to the existing ones that have already been specified in the instance for id.