on_entry and on_exit

The on_entry and on_exit annotations specify the effects of a library procedure on objects that are organized into data structures. We model data structures by adding edges between the objects. The edges are directed and can be roughly interpreted as ``points to''. Each identifier in these annotations is either an input to the procedure (a formal parameter), or gives a name to an object that is reachable by following edges from an input. Like the formal parameters, each name is arbitrary and is bound to actual objects at each procedure call site. The behavior of the procedure is summarized by showing the configuration before and after execution.

The -> operator indicates that the operand on the left points to the operand on the right. For example, in PLAPACK, each matrix parameter is passed as a pointer to a view structure, which in turn points to the underlying data. We can label an edge by providing an additional identifier followed by theof keyword. In the example, we label each edge from a view to its data with the label DATA. This distinguishes it from any other things that a view might point to. Figure  depicts the pointer structure given by the annotations labeled (4) in Figure .

  

Figure: The effect of split on PLAPACK data structures.

We can use the keyword null on the right side to indicate the removal of an edge.

The data structures described in these annotations need not correspond exactly to the underlying implementation. In fact, it is often useful to make explicit some of the relationships that are only represented implicitly in the implementation. Many libraries contain objects that behave logically like pointers, such as handles, references and descriptors. We can use on_entry and on_exit to model all of these structures.

In addition to establishing new data structures, the on_exit annotation can declare that an object is a copy of another object, using the copyof keyword. We can exploit this information to perform high-level copy propagation on library objects.