Atomicity violation detection using access interleaving invariants

1. A method of detecting atomicity violations in a program, the method comprising:

identifying, based on multiple executions of the program, multiple pairs of instructions that were intended to be executed atomically, the identifying multiple pairs of the instructions including a particular pair of instructions as one of the multiple pairs of instructions that were intended to be executed atomically only if atomicity of the particular pair of instructions is not violated during one of the multiple correct executions of the program;

identifying, during subsequent execution of the program, when a pair of instructions of the multiple pairs of instructions are to be executed and the atomicity of the pair of instructions violated, wherein identifying the atomicity of the pair of instructions is violated comprises:

accessing a cache line in a cache memory of a computing device that stores data for a memory location accessed by the pair of instructions, the cache line including:

an invalidate bit that is set when an interleaving remote write to the memory location occurs,

a downgrade bit that is set when the value in the memory location is a result of a previous write access by a local thread and the memory location has been read by a remote thread, and is cleared when the local thread accesses the memory location, and

a preceding access instruction bit that is set when the local thread performs a read access to the memory location, and is cleared when the local thread performs a write access to the memory location, and

using one or more of the invalidate bit, the downgrade bit, and the preceding access instruction bit to determine whether the atomicity of the pair of instructions is violated; and

detecting a bug as occurring in the program at the pair of instructions.

2. A method as recited in claim 1 , wherein identifying when a pair of the multiple pairs of instructions are to be executed and the atomicity of the pair of instructions violated comprises:

checking whether one instruction of the pair of instructions in the program is a read access instruction type or a write access instruction type;

if the one instruction is the read access instruction type, then detecting that the atomicity of the pair of instructions is violated based on whether there are any interleaving remote write accesses to a same location as accessed by the pair of instructions between the one instruction and a previous instruction of the pair of instructions; and

if the one instruction is the write access instruction type, then detecting that the atomicity of the pair of instructions is violated based on whether the previous instruction of the pair of instructions is the read access instruction type or the write access instruction type.

3. A method as recited in claim 1 , wherein identifying multiple pairs of instructions that were intended to be executed atomically comprises:

identifying, from the multiple executions of the program, a set of access interleaving invariants that are not violated during the multiple executions of the program; and

using the identified access interleaving invariants as a set of automatically extracted access interleaving invariants for the program.

4. A method as recited in claim 1 , wherein identifying the atomicity of the pair of instructions is violated comprises: maintaining a global access-owner table that stores an identifier of a thread that most recently wrote to each global memory location; maintaining, for each thread of the program, a local access table that stores information identifying whether a latest access by the thread to each global memory location was a read access or a write access; and using the global access-owner table and the local access tables to determine whether the atomicity of the pair of instructions is violated.

5. A method as recited in claim 1 , wherein using one or more of the invalidate bit, the downgrade bit, and the preceding access instruction bit to determine whether the atomicity of the pair of instructions is violated comprises:

if one instruction of the pair of instructions is a read access instruction type and the invalidate bit is set, then determine that the atomicity of the pair of instructions is violated;

if the one instruction of the pair of instructions is the read access instruction type and the invalidate bit is cleared, then determine that the atomicity of the pair of instructions is not violated;

if the one instruction of the pair of instructions is a write access instruction type and the preceding access instruction bit is set and the invalidate bit is set, then determine that the atomicity of the pair of instructions is violated;

if the one instruction of the pair of instructions is the write access instruction type and the preceding access instruction bit is set and the invalidate bit is cleared, then determine that the atomicity of the pair of instructions is not violated;

if the one instruction of the pair of instructions is the write access instruction type and the preceding access instruction bit is cleared and the downgrade bit is set, then determine that the atomicity of the pair of instructions is violated; and

if the one instruction of the pair of instructions is the write access instruction type and the preceding access instruction bit is cleared and the downgrade bit is cleared, then determine that the atomicity of the pair of instructions is not violated.

6. One or more non-transitory computer readable media having stored thereon instructions that detect atomicity violations in a program and that, when executed by one or more processors of a computing device, cause the one or more processors to:

check whether one instruction of a pair of instructions in the program is a read access instruction type or a write access instruction type, the pair of instructions comprising one of a set of access interleaving invariants having been generated by identifying multiple access interleaving invariants and including in the set of access interleaving invariants only ones of the multiple access interleaving invariants that are not violated during one of multiple correct executions of the program;

maintain a global access-owner table that stores an identifier of a thread that most recently wrote to each global memory location;

maintain, for each thread of the program, a local access table that stores information identifying whether a latest access by the thread to each global memory location was a read access or a write access;

use the global access-owner table and the local access tables to determine whether there are any interleaving remote write accesses to the same location as accessed by the pair of instructions between the one instruction and a previous instruction of the pair of instructions;

if the one instruction is the read access instruction type, then detect an atomicity violation at the pair of instructions based on whether there are any interleaving remote write accesses to the same location as accessed by the pair of instructions between the one instruction and the previous instruction of the pair of instructions; and

if the one instruction is the write access instruction type, then detect an atomicity violation at the pair of instructions based on whether the previous instruction of the pair of instructions is the read access instruction type or the write access instruction type.

7. The one or more computer readable media as recited in claim 6 , wherein to check whether the one instruction is a read access instruction type or a write access instruction type is to check whether the one instruction is a read access instruction type or a write access instruction type only if the one instruction is an I-instruction of an access interleaving invariant.

8. The one or more computer readable media as recited in claim 6 , wherein to detect an atomicity violation at the pair of instructions based on whether there are any interleaving remote write accesses between the one instruction and the previous instruction of the pair of instructions is to:

check whether there are any interleaving remote write accesses between the one instruction and the previous instruction of the pair of instructions;

if there are not any interleaving remote write accesses between the one instruction and the previous instruction of the pair of instructions then detect that no atomicity violation occurs at the pair of instructions; and

if there is at least one interleaving remote write access between the one instruction and the previous instruction of the pair of instructions then detect that an atomicity violation occurs at the pair of instructions.

9. The one or more computer readable media as recited in claim 6 , wherein to detect an atomicity violation at the pair of instructions based on whether the previous instruction of the pair of instructions is the read access instruction type or the write access instruction type is to:

check whether the previous instruction is the read access instruction type or the write access instruction type;

if the previous instruction is the read access instruction type, then:

check whether there are any interleaving remote write accesses between the one instruction and the previous instruction of the pair of instructions;

if there are not any interleaving remote write accesses between the one instruction and the previous instruction of the pair of instructions then detect that no atomicity violation occurs at the pair of instructions; and

if there is at least one interleaving remote write access between the one instruction and the previous instruction of the pair of instructions then detect that an atomicity violation occurs at the pair of instructions; and if the previous instruction is the write access instruction type, then:

check whether any interleaving remote read access gets a result of the previous instruction;

if no interleaving remote read access gets the result of the previous instruction, then detect that no atomicity violation occurs at the pair of instructions; and

if there is at least one interleaving remote read access that gets the result of the previous instruction, then detect that an atomicity violation occurs at the pair of instructions.

10. One or more non-transitory computer readable media having stored thereon instructions that automatically extract access interleaving invariants in a program and that, when executed by one or more processors of a computing device, cause the one or more processors to:

identify, from multiple correct executions of the program, a set of access interleaving invariants that are not violated during the multiple correct executions of the program, wherein an access interleaving invariant is to be included in the set of access interleaving invariants only if the access interleaving invariant is not violated during one of the multiple correct executions of the program, and wherein to identify the set of access interleaving invariants is to:

create a current set of possible access interleaving invariants in the program,

for each execution of the program, detect whether any access interleaving invariants are violated at least a first threshold number of times and remove any access interleaving invariants that are violated at least the first threshold number of times from the current set,

repeat execution of the program until the program is executed at least a second threshold number of times without any changes to the current set of possible access interleaving invariants, and

remove, after the program is executed at least the second threshold number of times without any changes to the current set of possible access interleaving invariants, any access interleaving invariants including instructions that were never executed during the execution of the program; and

use the identified access interleaving invariants as a set of automatically extracted access interleaving invariants for the program.

11. The one or more computer readable media as recited in claim 10 , wherein the first threshold number of times comprises one time.

12. The one or more non-transitory computer readable media as recited in claim 10 , wherein to identify the set of access interleaving invariants that are not violated during the multiple executions of the program is to:

check whether one instruction of a pair of instructions in the program is a read access instruction type or a write access instruction type;

if the one instruction is the read access instruction type, then determine whether an access interleaving invariant including the one instruction is violated based on whether there are any interleaving remote write accesses to a same location as accessed by the pair of instructions between the one instruction and a previous instruction of the pair of instructions; and

if the one instruction is the write access instruction type, then determine whether an access interleaving invariant including the one instruction is violated based on whether the previous instruction of the pair of instructions is the read access instruction type or the write access instruction type.

13. A computing device comprising:

a processor;

a cache memory storing data organized by cache line, each cache line having associated with it a downgrade bit and a preceding access instruction bit, and wherein for each cache line:

the downgrade bit of the cache line is set when data in the cache line is a result of a previous write access by a local thread and the cache line has been read by a remote thread,

the downgrade bit of the cache line is cleared when the local thread accesses the cache line,

the preceding access instruction bit of the cache line is set when the local thread performs a read access to the cache line, and

the preceding access instruction bit of the cache line is cleared when the local thread performs a write access to the memory location;

the each cache line being associated with a thread identifier to identify which of a plurality of threads of a program being executed by the processor most recently accessed the cache line; and

a set of instructions to use the downgrade bit, the preceding access instruction bit, and the thread identifier to detect atomicity violations in the program being executed by the processor.

14. A computing device as recited in claim 13 , wherein the set of instructions use the downgrade bit and the preceding access bit to detect atomicity violations as follows:

if one instruction of a pair of instructions in the program is a read access instruction type and an invalidate bit of the cache line accessed by the one instruction is set, then determine that the atomicity of the pair of instructions is violated;

if the one instruction of the pair of instructions is the read access instruction type and the invalidate bit is cleared, then determine that the atomicity of the pair of instructions is not violated;

if the one instruction of the pair of instructions is a write access instruction type and the preceding access instruction bit is set and the invalidate bit is set, then determine that the atomicity of the pair of instructions is violated;

if the one instruction of the pair of instructions is the write access instruction type and the preceding access instruction bit is set and the invalidate bit is cleared, then determine that the atomicity of the pair of instructions is not violated;

if the one instruction of the pair of instructions is the write access instruction type and the preceding access instruction bit is cleared and the downgrade bit is set, then determine that the atomicity of the pair of instructions is violated; and

if the one instruction of the pair of instructions is the write access instruction type and the preceding access instruction bit is cleared and the downgrade bit is cleared, then determine that the atomicity of the pair of instructions is not violated.

15. A computing device as recited in claim 14 , wherein the one instruction of the pair of instructions in the program is encoded to identify the one instruction as an I-instruction, and to indicate that a check as to whether there is an atomicity violation at the pair of instructions is to be performed.

16. A computing device as recited in claim 13 , each cache line having associated with it multiple downgrade bits and multiple preceding access instruction bits, each of the multiple downgrade bits being associated with one of multiple words in the cache line, and each of the multiple preceding access instruction bits being associated with one of the multiple words in the cache line.