Communications - June 2010

Checking this specification is a kind of regression testing. In particular, if the code change has introduced a regression— i.e., a bug that causes the new code to produce a semantically different output then the old code for some input—then the above specification does not hold.

Further, we believe there is a wider class of program properties that are easy to write in bridge assertions but would be quite difficult to write otherwise. For example, consider the specification:

deterministic assume( set.size() == set¢.size()) {
P
} assert ( set.size () == set¢.size ());

This specification requires that sequential or parallel program block P transforms set so that its final size is some function of its initial size, independent of its elements. The specification is easy to write even in cases where the exact relationship between the initial and final size might be quite complex and difficult to write. It is not entirely clear, however, when such properties are important or useful to specify.

7. concLusion

We have proposed bridge predicates and bridge assertions for specifying the user-intended semantic deterministic behavior of parallel programs. We argue that our specifications are much simpler for programmers to write than traditional specifications of functional correctness, because they enable programmers to compare pairs of program states across different executions rather than relating program outputs directly to program inputs. Thus, bridge predicates and bridge assertions can be thought of as a lightweight mechanism for specifying the correctness of just the parallelism in a program, independently of the program’s functional correctness.

We have shown experimental evidence that we can effectively check our deterministic specifications. In particular, we can use existing techniques for testing parallel software to generate executions exhibiting data and higher-level races. Then our deterministic specifications allow us to distinguish from the benign races the parallel nondeterminism bugs that lead to unintended nondeterministic program behavior. Thus, we argue that it is worthwhile for programmers to write such lightweight deterministic specifications. In fact, later work6 has suggested that, given the simple form of our specifications, it may often be possible to automatically infer likely deterministic specifications for parallel programs.

acknowledgments

We would like to thank Nicholas Jalbert, Mayur Naik,
Chang-Seo Park, and our anonymous reviewers for their
valuable comments on previous drafts of this paper. This
work supported in part by Microsoft (Award #024263) and
Intel (Award #024894) funding and by matching funding by
U.C. Discovery (Award #DIG07–10227), by NSF Grants CNS-
0720906 and CCF-0747390, and by a DoD NDSEG Graduate
Fellowship.

1. Artho, C., Havelund, k., biere, A. High-level data races. Softw. Test. ver. reliab. 13, 4 (2003), 207–227.

2. Asanovic, k., bodik, R., Demmel, J., keaveny, T., keutzer, k., kubiatowicz, J.D., Lee, E.A., Morgan, n., necula, g., Patterson, D.A., Sen, k., Wawrzynek, J., Wessel, D., yelick, k. A. The Parallel Computing Laboratory at u.C. Berkeley: A research Agenda Based on the Berkeley view. Technical Report uCb/EECS-2008–23, EECS Department, university of California, berkeley, March 2008.

3. barnes, g. A method for implementing lock-free shared-data structures. In 5th ACM Symposium on Parallel Algorithms and Architectures (SPAA) (1993).

4. bocchino, R.L., Jr., Adve, V.S., Dig, D., Adve, S.V., Heumann, S., komuravelli, R., overbey, J., Simmons, P., Sung, H., Vakilian, M. A type and effect system for deterministic parallel

Java. In 24th ACM SIGPLAn
Conference on Object-Oriented
Programming Systems, Languages
and Applications (OOPSLA) (2009).
5. burnim, J., Sen, k. Asserting
and checking determinism for
multithreaded programs. In 7th
Joint Meeting of the European
Software Engineering Conference
and the ACM SIGSOFT Symposium
on the Foundations of Software
Engineering (ESEC/FSE) (2009).
6. burnim, J. Sen, k. DETERMIn:
Inferring likely deterministic
specifications of multithreaded
programs. In 32nd ACM/IEEE
International Conference on
Software Engineering (ICSE) (2010).

7. Edelstein, o., Farchi, E., nir, y., Ratsaby, g., ur, S. Multithreaded Java program test generation. IBM Syst. J. 41, 1 (2002), 111–125.

8. Flanagan, C., Freund, S.n. Atomizer: A dynamic atomicity checker for multithreaded programs. In 31st ACM SIGPLAn-SIGAC T Symposium on Principles of Programming Languages (POPL) (2004).

9. Flanagan, C., Qadeer, S. A type and effect system for atomicity. In ACM SIGPLAn 2003 Conference on Programming Language Design and

Implementation (PLDI) (2003).
10. Johnston, W.M., Hanna, J.R.P.,
Millar, R.J. Advances in dataflow
programming languages. ACM
Comput. Surv. 36, 1 (2004),
References

Jacob Burnim ( jburnim@cs.berkeley.edu), EECS Department, uC berkeley, CA.

1–34.

11. kaminsky, A. Parallel Java: A unified API for shared memory and cluster parallel programming in 100% Java. In 21st IEEE International Parallel and Distributed Processing Symposium (IPDPS) (2007).

12. Lee, E.A. The problem with threads. Computer 39, 5 (May 2006), 33–42.

13. Loidl, H., Rubio, F., Scaife, n., Hammond, k., Horiguchi, S., klusik, u., Loogen, R., Michaelson, g., Pena, R., Priebe, S. et al. Comparing parallel functional languages: Programming and performance. High. Order Symb. Comput. 16, 3 (2003), 203–251.

14. Park, C.-S., Sen, k. Randomized active atomicity violation detection in concurrent programs. In 16th ACM SIGSOF T International Symposium on Foundations of Software Engineering (FSE) (2008).

15. Sadowski, C., Freund, S., Flanagan, C. Single Track: A dynamic determinism checker for multithreaded programs. In 18th European Symposium on Programming (ESOP) (2009).

16. Sen, k. Race directed random testing of concurrent programs. In ACM SIGPLAn Conference on Programming Language Design and Implementation (PLDI'08) (2008).

17. Smith, L.A., bull, J.M., obdrzálek, J. A parallel java grande benchmark suite. In ACM/IEEE Conference on Supercomputing (SC) (2001).

18. Stoller, S.D. Testing concurrent Java programs using randomized scheduling. In 2nd Workshop on runtime verification (rv) (2002).

19. Thies, W., karczmarek, M., Amarasinghe, S. StreamIt: A language for streaming applications. In 11th International Conference on Compiler Construction (CC) (2002).

20. Visser, W., Havelund, k., brat, g., Park, S., Lerda, F. Model checking programs. Autom. Softw. Eng. 10, 2 (2003), 203–232.

21. von Praun, C., gross, T.R. object race detection. In 16th ACM SIGPLAn Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (2001).