semantic Determinism: The above deterministic specification is often too conservative. For example, consider a similar example, but where A,B,and Care floating-point matrices:

deterministic {
C = parallel_matrix_multiply_float(A, B);
}

Limited-precision floating-point addition and multiplication are not associative due to rounding error. Thus, depending on the implementation, it may be unavoidable that the entries of matrix C will differ slightly depending on the thread schedule.

In order to tolerate such differences, we must relax the deterministic specification:

deterministic {
C = parallel_matrix_multiply_float(A, B);
} assert(|C − C¢| < 10− 6);

This assertion specifies that, for any two matrices C and C¢ resulting from the execution of the matrix multiply from the same initial state, the entries of C and C¢ must differ by only a small quantity (i.e., 10− 6).

Note that the above specification contains a predicate over two states—each from a different parallel execution of the deterministic block. We call such a predicate a bridge predicate, and an assertion using a bridge predicate a bridge assertion. Bridge assertions are different from traditional assertions in that they allow one to write a property over two program states coming from different executions whereas traditional assertions only allow us to write a property over a single program state.

Note also that such predicates need not be equivalence relations on pairs of states. In particular, the approximate equality used above is not an equivalence relation.

This relaxed notion of determinism is useful in many contexts. Consider the following example which adds in parallel two items to a synchronized set:

Set set = new SynchronizedTreeSet(); deterministic { } assert(set.equals(set¢));

If set is represented internally as a red–black tree, then a strict deterministic assertion would be too conservative. The structure of the resulting tree, and its layout in memory, will likely differ depending on which element is inserted first, and thus different parallel executions can yield different program states.

But we can use a bridge predicate to assert that, no matter what schedule is taken, the resulting set is semantically

the same. That is, for objects set and set¢ computed by two different schedules, the equals method must return true because the sets must logically contain the same elements. We call this semantic determinism.

Preconditions for Determinism: So far we have described the following construct:

deterministic {
P
} assert(Post);

where Post is a predicate over two program states from different executions with different thread schedules. That is, if s and s¢ are two states resulting from any two executions of P from the same initial state, then Post (s, s¢) holds.

The above construct could be rewritten:

deterministic assume(s0 = s0¢) {
P
} assert(Post);

That is, if any two executions of P start from initial states s0 and s0¢, respectively, and if s and s¢ are the resulting final states, then s0 = s0¢ implies that Post (s, s¢) holds. The above rewritten specification suggests that we can relax the requirement of s0 = s0¢ by replacing it with a bridge predicate Pre (s0, s0¢). For example:

 

deterministic assume(set.equals(set¢)) { set.add( 3); || set.add( 5);

} assert(set.equals(set¢) );

 

The above specification states that if any two executions start from sets containing the same elements, then after the execution of the code, the resulting sets must also contain the same elements.

Comparison to Traditional Assertions: In summary, we propose the following construct for the specification of deterministic behavior:

deterministic assume(Pre) {
P
} assert(Post);

Formally, it states that for any two program states s0 and s0¢, if ( 1) Pre (s0, s0¢) holds, ( 2) an execution of P from s0 terminates and results in state s, and ( 3) an execution of P from s0¢ terminates and results in state s¢, then Post (s, s¢) must hold.

Note that the use of bridge predicates Pre and Post has the same flavor as pre- and postconditions used for functions in program verification. However, unlike traditional pre- and postconditions, the proposed Pre and Post predicates relate pairs of states from two different executions. In traditional verification, a precondition is usually written as a predicate over