The current implementation of 2SP is an interpreter (approx.
6,000 lines of SML'97 code, using Standard ML of New Jersey).
The interpreter and several different application examples (from
simple to complex) are immediately available at http://www.ifi.unibas.ch/Research/Coordination_Models/2sp/2sp.html
(without downloading and installing any software). Two complex
applications are also detailed in [3,
4].
Basic Features
We describe the basic idea of the 2SP approach through the
simple example of Fibonacci numbers to facilitate a fast understanding.
Figure 1 shows
the 2SP program for computing the
nth Fibonacci
number. Fibonacci numbers are described by the standard recursive
definition:
0 specification (* fib.spc *)
1 n = (* ... *) ;
2 fib (i) = if i = 0 then 0
3 else if i = 1 then 1
4 else if i > 1 then
5 fib.l1(i-1)+fib.l2(i-2)
6 endif
7 endspecification
8 coordination (* fib.cor *)
9 A := fib (0) ;
10 B := fib (1) ;
11 for i count n-1 from 2 do
12 C := fib (i) | fib.l1 <- B ^ fib.l2 <- A ;
13 A := fib (i-1) <- B ;
14 B := fib (i) <- C
15 endfor
16 endcoordination
Figure 1: A simple 2SP program.
The first part of a 2SP program is a specification.
It is purely functional, store independent. In the above case,
the specification directly describes the standard definition.
The only unusual aspect of the specification is the presence
of the labels l1 and l2 (Line 5). Labels identify
different applications of the same function. Their sole purpose
is to enable a coordination to uniquely refer to a particular
function application in a given definition. The second part of
a 2SP program is a coordination. The above coordination
maps the recursive definition to the following standard imperative
program:
A := 0; B := 1; i := 2;
while i < n + 1 do
C := B + A; A := B; B := C; i := i+1
end
After termination of execution, store B contains fn
for n > 0. It is possible to have several coordinations
for a single specification, each of them implementing a different
algorithm.
Function Applications 2SP includes
three sorts of function applications that make it different from
any other programming language:
- (1) Full application:
- The function applications fib(0) and fib(1)
(Lines 9 and 10, respectively) are called full applications.
They evaluate by simply following the corresponding recursive
function definition. This kind of function application offers
the possibility to directly execute the specification (in general
not efficient, but useful to validate the specification---rapid
prototyping);
-
- (2) Fetch Application:
- The function applications fib(i-1) <- B (Line
13) and fib(i) <- C (Line 14) are called fetch applications.
They evaluate by retrieving the function values fib(i - 1)
and fib(i) from stores B and C, respectively
(provided these stores contain the required values).
-
- (3) Step Application:
- The function application on Line 12 is called step application
(fib(i) | fib.l1 <- B ^ fib.l2 <- A). It executes
a single step of the recursive evaluation. Values fib(i -
1) and fib(i - 2) needed to compute fib(i),
for i > 1, are not determined by following again
the recur sive definition. They are fetched from the stores B
and A, respectively (again, provided these stores contain
those values). The utility of the labels is clear now. A step
application always refers to a function definition while a fetch
application does not.
Assignment commands, full, fetch, and step applications provide
the so called consistency link between specification and
coordination. This is the base of a powerful mechanism for checking
consistency (the consistency checker), described below.
The Consistency Checker The consistency
checker checks, at run-time, whether the stores, from which value
retrievals are performed, actually contain the desired values.
The computation is aborted and a detailed error message is displayed
in case of mismatch. The check is performed by means of symbolic
names (called value names) associated with values. For
example, the pair (fib,i) is a value name
of the value fib(i), where fib is some encoding
of the function identifier fib. A corresponding value
name is always stored together with the value, after executing
an assignment command. When fetching the value from a store,
a comparison between the expected value name (provided by the
programmer through fetch or step applications) and the stored
value name is performed. If both value names agree, the value
is fetched, otherwise execution aborts, and an error message
is displayed. The error message contains additional information
(provided by the value names) and substantially helps debugging.
Consider a typical programming error: an error in the range of
a loop-counter. For example, if Line 11 is erroneously written:
for i count n from 1 do, the following error message
is generated:
Error: value name mismatch in step application
Line: 12
Store: B @ ROOT
Value name expected: fib (0)
Value name found: fib (1)
ROOT is the name of the default processor that runs
the program and owns store B. The operator ``@"
means ``at". The corresponding standard imperative program
(see above), with this error, terminates normally, but produces
a wrong result: store B stores fn+1
instead of fn, as required. No need to discuss
the consequences of such a wrong, undetected result used later
for a critical decision!
Related Work
The result-checking approach is to check the correctness of
the final result after execution of a program [2].
The advantage of this approach is that, after the execution,
the user knows (with sufficient probability) whether the result
is correct or not. Both, result-checking approach and 2SP, use
checkers. The checker used by the result-checking approach is
external, built separately from the program. The checker used
by 2SP is internal, built together with the program. The result-checking
approach treats programs as black boxes and, therefore, offers
support to only detect errors, but not to locate them. In contrast,
2SP offers strong support to precisely detect and locate
errors.
References
[1] Lyu, M. R. "Handbook
of Software Reliability Engineering". McGraw-Hill, 1996.
[2]
Wassermann, H.; Blum, M. "Software Reliability via Run-Time
Result-Checking".
Journal of the ACM, 44(6):826--849,
November 1997
[3]
Lederer, E. F. A.; Dumitrescu, R. A.
"Specification-Consistent
Coordination Model for Computations," 122-129.
Proceedings
of the 13th ACM Symposium on Applied Computing (SAC'98).
Special Track on Coordination Models, Languages, and Applications.
ACM Press, Atlanta, U. S. A., February 27-March 1, 1998.
[4]
Lederer, E. F. A.; Dumitrescu, R. A.
"Two-Stage
Programming," 296-311.
Proceedings of the Third Fuji
International Symposium on Functional and Logic Programming (FLOPS'98).
Kyoto University, Kyoto, JAPAN, April 2-4, 1998.
