Static verification of parallel program code

摘要

A symbolic encoding of predicated execution for static verification, based on a plurality of data parallel program instructions, is obtained. A result of static verification of one or more attributes associated with the plurality of data parallel program instructions is obtained, based on the symbolic encoding.

主权项

1. A system comprising:
at least one hardware device processor; a symbolic encoding component that obtains a symbolic encoding of predicated execution for static verification, by obtaining a translated program that includes a plurality of data parallel program instructions, the translated program translated to a form modeling the predicated execution of two arbitrary and distinct threads and instrumented with calls to executable procedures configured to log accesses to shared memory locations by logging an indicator of a location that is accessed, and which of the two threads is responsible for the logged accesses, and a current enablement status for each of the two threads at a time of the logged accesses; and a static verification component that obtains, via the at least one device processor, a result of static verification of one or more attributes associated with the plurality of data parallel program instructions, based on the symbolic encoding, and on results of one or more assertions of a barrier procedure that a pair of predicate values indicate a same state of enablement for the threads using boolean operations, to indicate whether the threads are both enabled at a time of the one or more assertion the barrier procedure, on results of one or more of the logged accesses.