Automatic verification of determinism for parallel programs
AssigneeInternational Business Machines Corporation
InventorsMartin Vechev, Eran Yahav, Raghavan Raman, Vivek Sarkar
Life of this patent
Estimating the term…
Abstract
Automatic verification of determinism in structured parallel programs includes sequentially establishing whether code for each of a plurality of tasks of the structured parallel program is independent, outputting sequential proofs corresponding to the independence of the code for each of the plurality of tasks and determining whether all memory locations accessed by parallel tasks of the plurality of tasks are independent based on the sequential proofs.
Claims12
A computer program product for automatically verifying determinism of a structured parallel program, the computer program product comprising:
- a non-transitory computer readable storage medium having computer readable program code embodied therewith, the computer readable program code comprising:
- computer readable first program code configured to sequentially establish whether second program code in each of a plurality of tasks of the structured parallel program is independent, configured to output sequential proofs corresponding to the independence of the second program code in each of the plurality of tasks and configured to determine whether all memory locations accessed by the plurality of tasks are independent based on the sequential proofs,
- wherein the first program code determines for each second program code whether a first program label is present within the second program code that accesses a same array via an index variable within the second program code,
- wherein the first program code determines for each index variable all values the corresponding index variable is capable of reaching using at least one second program label within the corresponding second program code to determine an over-approximated range of values,
- wherein each range is represented as a linear inequality using the corresponding index variable;
- and
- wherein the first program code determines two or more of the second programs codes are independent when the determined ranges are non-overlapping with respect to the same array.
A system for automatically verifying determinism of a structured parallel program comprising:
- a memory device storing a plurality of instructions embodying the system for automatically verifying determinism of structured parallel programs;
- and
- a processor configured to execute the plurality of instructions to perform a method comprising:
- establishing, sequentially, whether program code in each of a plurality of tasks of the structured parallel program is independent;
- outputting sequential proofs corresponding to the independence of the program code in each of the plurality of tasks;
- and
- determining whether all memory locations accessed by the plurality of tasks are independent based on the sequential proofs,
- wherein the establishing:
- determines for each program code whether a first program label is present within the program code that accesses a same array via an index variable within the program code,
- determines for each index variable all values the corresponding index variable is capable of reaching using at least one second program label within the corresponding program code to determine an over-approximated range of value,
- determines whether two or more of the program codes are independent when the determined ranges are non-overlapping with respect to the same array, and
- wherein each range is represented as linear inequality using the corresponding index variable.
Dependencies are inferred from the claim text.