Lightweight specifications for parallel correctness

摘要: With the spread of multicore processors, it is increasingly necessary for programmers to write parallel software. Yet writing correct software with explicit multithreading remains a difficult undertaking. Though many tools exist help test, debug, and verify programs, such are often hindered by lack any specification from programmer intended, behavior his or her software. In this dissertation, we propose three novel lightweight specifications parallelism correctness multithreaded software: semantic determinism, atomicity, nondeterministic sequential correctness. Our determinism enable specify that run program on same input should deterministically produce output, despite interleaving program's threads execution. Key our proposed bridge predicates . compare pairs states different executions equivalence. atomicity use generalize traditional enabling regions concurrent are, at high-level, free harmful interference other threads. Finally, (NDSeq) completely but version and, further, functional sequentially, program. We show us much more effectively specify, in software, independent complex fundamentally-sequential We can easily number Java benchmarks. testing techniques checking conforms its specification, apply these find errors Further, automatically inferring likely NDSeq program, given handful representative executions.