Name
Title | ||
|---|---|---|
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses |
Abstract | ||
|---|---|---|
Transactional memoryis a programming abstraction intended to simplify the synchronization of conflicting memory accesses (by concurrent threads) without the difficulties associated with locks. In a previous work we presented a formal framework for proving that a transactional memory implementation satisfies its specifications and provided with model checking verification of some using small instantiations. This paper extends the previous work to capture non-transactional accesses to memory, which occurs, for example, when using legacy code. We provide a mechanical proof of the soundness of the verification method, as well as a mechanical verification of a version of the popular tccimplementation that includes non-transactional memory accesses. The verification is performed by the deductive temporal checker tlpvs. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-70545-1_13 | CAV |
Keywords | Field | DocType |
non-transactional access,transactional memory implementation,previous work,verification method,model checking verification,transactional memoryis,mechanical verification,non-transactional memory accesses,non-transactional memory access,conflicting memory access,transactional memories,mechanical proof,transactional memory,model checking | Software transactional memory,Programming language,Computer science,Parallel computing,Cache-only memory architecture,Transactional memory,Memory model,Memory management,Memory map,Flat memory model,Distributed shared memory | Conference |
Volume | ISSN | Citations |
5123 | 0302-9743 | 10 |
PageRank | References | Authors |
0.56 | 7 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ariel Cohen | 1 | 86 | 5.63 |
| Amir Pnueli | 2 | 12964 | 2377.59 |
| Lenore D. Zuck | 3 | 1559 | 141.69 |