-- -- graph e is a binary edge relation -- program fastcycle; read(e); -- read the set e of edges refcount := {}; -- code to establish invariant refcount for x1 in domain e loop for c1 in e{x1} loop if refcount(c1) = om then refcount(c1) := 1; else refcount(c1) +:= 1; end if; end loop; end loop; zeroset := {}; for x2 in domain e loop if x2 notin domain refcount then zeroset with:= x2; -- refcount(x2) = om <-> refcount(x2) = 0 end if; end loop; while exists u in zeroset | true loop for c2 in e{u} loop -- code to reestablish refcount and zeroset if c2 in domain e and refcount(c2) = 1 then zeroset with:= c2; end if; refcount(c2) -:= 1; end loop; zeroset less := u; -- reestablish zeroset e(u) := om; end loop; print(domain e /= {}); end;

A method is sketched for simulating each primitive set and map operation in realtime on a RAM (i.e., each set operation is implemented in unit worst case time on a RAM). The method will only work on a highly restrictive class of SETL2 programs that read all of their input at the beginning of execution. To use the method on any program outside of this class, we need to transform that program into an equivalent program inside the class.

The simulation method depends on the assumption that each data value in a SETL2 program must belong to a set denoted by a type. For convenience, we require the much stronger restriction that each distinct program variable v must store values in a set denoted by some type tau throughout the execution of the program. Such a program invariant is specified by a type assignment v: tau.

Consider the following simple type system, where each type TAU represents a set val(TAU). Type INT stands for the set of integers. If TAU is a type, then type SET(TAU) represents the set of finite subsets of val(TAU). If TAU1 and TAU2 are types, then smap(TAU1,TAU2) and mmap(TAU1,TAU2) represent the set of finite partial single-valued (resp. multi-valued) maps from domain val(TAU1) to range val(TAU2). Variables B are called base types, each of which is uniquely associated with a subtype constraint of the form B < TAU (where TAU is any type except for a base type), which indicates that val(B) is a subset of val(TAU).

For any program, each of its variables v must have a type assignment of the form v: TAU, and every base type B must be associated with a subtype constraint of the form B < TAU1. The subtype constraints for a given program are restricted so that the graph

{[B1,B2]: B1 < TAU2 is a subtype constraint and base type B2 occurs in TAU2}

is acyclic. Later, we will see how to calculate val(B) for any base type B as a finite set of values obtained from the input and from program constants.

Besides representing specific sets, each type is also used to model specific data structures needed to implement set and map operations efficiently. For this purpose, we augment the type system slightly by allowing a base type B to appear in two forms: (1) (weak) B, and (2) (strong) B-strong. Three kinds of data structures are considered - unbased, weakly based, and strongly based - see figures for unbased, weakly based, and strongly based representations(best viewed in printed form, because the ghostview images of these files are not accurate).

If TAU and TAU1 are any types except for base variables, and if TAU2 is any type except for strong base variables, then unbased sets are denoted by type set(TAU), and unbased single- and multi- valued maps are denoted by smap(TAU1,TAU2) and mmap(TAU1,TAU2) respectively (where TAU1 is the domain element type and TAU2 is the range element type). If B is a base type with subtype constraint B < TAU, then weakly based sets are denoted by set(B), and weakly based maps are denoted by smap(B,TAU2) and mmap(B,TAU2). Strongly based sets are denoted by set(B-strong); strongly based maps are denoted by smap(B-strong,TAU2) and mmap(B-strong,TAU2). Strongly based types are restricted to program variables, and can appear only in type assignments (and not in subtype constraints).

One final restriction must be made so that the sets represented by base types only contain values obtained directly from the input. First we itemize every program variable (and the domain and range of every map) together with the operations on it. These operations are categorized into INITIALIZE (for assigning input or constants to variables), RETRIEVE, ACCESS (or SELFACCESS in the case where the search argument is always retrieved from the same set that is subsequently accessed), ADD, and DELETE. We represent these operations as edges that appear as comments just after each set operation in the program below.

x ACCESS> y means that x is used to access set y; e.g. x in y

x SELFACCESS> y is a simplified form of access that requires no search, because x was originally retrieved from y

y RETRIEVE> x means that x is retrieved from set y; e.g., exists x in y

x ADD> y means that x is added to set y; e.g., y with:= x

x DELETE> y means that x is delected from y; e.g., y less:= x

x INITIALIZE> y means that y is assigned to x, where x is either input or a program constant; e.g., read(y), where x = INPUT

Sufficient conditions for real-time simulation are given by the following rules:

- (ACCESS) For each edge of the form x ACCESS> y, the element type of y is B-strong for some finite set B. This rule supports unit time associative access.
- (COMPATIBILITY) For every edge of the form x ACCESS> y, x ADD> y, or x DELETE> y, where the element type of y is B (or B-strong), then x is of type B; for every edge of the form y RETRIEVE> x, where x is of type B, then the element type of y must also be of type B. This rule is a consequence of rule 1.
- (SIMPLICITY) Any based representation that isn't the strong representation is the weak representation. This rule prefers the simpler weakly based structure to the strongly based one.
- (DESTRUCTIVE UPDATE) If there are operations of either form y ADD> x or y DELETE> x, then there can be no operation of the form x ADD> w, x DELETE> w, or x ACCESS> w. This rule allows destructive updates without violating copy/value semantics.
- (STATIC BASE) No value with base type can result from any arithmetic operation. Together with the other rules, this rule ensures that base types represent finite sets obtained directly from the input and from program constants.

When all of the preceding conditions are satisfied, then for each base type B, val(B) is defined to be the smallest set that satisfies the program type assignments (restricted to input variables), the program subtype constraints, and the defined correspondences between types and the sets they denote.

For example, let us calculate the sets represented by base types A and I in a program with type assignments

X:set(A), F: mmap(I,A)and subtype constraints

A < INT, I < set(A)From the type assignments we get the constraints,

1. {X} subset val(set(A)), and 2. {F} subset val(mmap(I,A))where X and F are the runtime input values. From the subtype constraints we obtain two more constraints,

3. val(A) subset val(INT) 4. val(I) subset val(set(A))From the definition of val, val(set(A)) = {S: S subset val(A) | A is finite}, we can replace constraint (1.) by the simpler constraint,

1. X subset val(A)Likewise, constraint (2.) can be replaced by two constraints

2a. domain F subset val(I), and 2b. range F subset val(A)Finally, constraint (4.) can be simplified to,

4. +/val(I) subset val(A)where +/val(I) computes the union of all the set valued elements of val(I).

The solution is now clear. The smallest value of val(I) is domain F at input time; the smallest value of val(A) is the union of range F, X, and +/(domain F) for X and F at input time.

Below we apply the method to simulate a low level SETL2 cycle testing program in real-time.

program fastcycle; read(e); --input initialize> e (domain e, range e) refcount := {}; --{} initialize> refcount (domain refcount, range refcount) for x1 in domain e loop --domain e retrieve> x1 for c1 in e{x1} loop --x1 selfaccess> domain e --range e retrieve> c1 if refcount(c1) = om then --c1 access> domain refcount refcount(c1) := 1; --c1 selfaccess> domain refcount --c1 add> domain refcount else refcount(c1) +:= 1; --c1 selfaccess> domain refcount end if; end loop; end loop; zeroset := {}; --{} initialize> zeroset for x2 in domain e loop --domain e retrieve> x2 if x2 notin domain refcount then --x2 access> domain refcount zeroset with:= x2; --x2 add> zeroset end if; end loop; while exists u in zeroset | true loop --zeroset retrieve> u for c2 in e{u} loop --u access> domain e --range e retrieve> c2 if c2 in domain e and refcount(c2) = 1 then --c2 access> domain e --c2 access> domain refcount zeroset with:= c2; --c2 add> zeroset end if; refcount(c2) -:= 1; --c2 selfaccess> domain refcount end loop; zeroset less := u; --u selfaccess> zeroset --u delete> zeroset e(u) := om; --u selfaccess> domain e --u delete> domain e end loop; print(domain e /= {}); end;With the following type assignments,

zerocount: set(B-strong) e: map(B-strong,B) refcount: map(B-strong,int) x1,x2,c1,c2,u: B

the subtype constraint

B < INT (which means that nodes are represented by integers)the preceding program satisfies the five sufficient conditions for realtime simulation, and B = domain e U range e.

More efficient data structures than the general ones modeled by our type system can be obtained by removing linked structures that are never used by the program. This approach yields the following data structures, which are drawn here.

zeroset is a one-way list with a first but not a last finger;

domain refcount will not be a linked list;

domain e is a doubly linked list, and each image e{x} is a one way linked list for x in domain e; each of the lists in e has a first but not a last finger

HINT: In your homework, linked lists will have to be represented in terms of arrays (dynamically allocated but static tuples).