Details

Autor(en) / Beteiligte

• Sangwine Stephen J
• Qadri Muhammad Yasir
• Qadri, Muhammad Yasir
• Sangwine, Stephen J.

Titel

Verified Multicore Parallelism Using Atomic Verifiable Operations

Ist Teil von

• Multicore Technology, 2014, p.133-178

Ort / Verlag

CRC Press

Erscheinungsjahr

2014

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Michal Dobrogost, Christopher Kumar Anand, and Wolfram KahlDepartment of Computing and Software, McMaster University, Hamilton, Ontario, Canada4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 4.1.1 Novelty . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 4.1.2 Impact . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 4.1.3 Chapter Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1104.2 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 4.2.1 Map Modification Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 4.2.2 Groups . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 4.2.3 Disjoint Unions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1124.3 Background and Previous Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 4.3.1 Concurrency Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 4.3.2 Motivating Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 4.3.3 Strictly Forward Inspection of Partial Order . . . . . . . . . . . 116 4.3.4 The Follows Map (Φ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 4.3.5 Φ Slices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 4.3.6 Discussion of the Follows Map (Φ) . . . . . . . . . . . . . . . . . . . . . . 119 4.3.7 Merging Φ Slices to Strengthen Our Partial Order . . . . . 121 4.3.8 State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 4.3.9 Verification Step . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1224.4 The Loop AVOp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 4.4.1 Loop AVOp Indexing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124 4.4.2 Loop Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1254.5 Efficient Verification of Looping Programs . . . . . . . . . . . . . . . . . . . . . . 126 4.5.1 Locally Sequential Loops . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 4.5.2 Bumping State to the Next Iteration via Λ . . . . . . . . . . . . . 127 4.5.3 Loop Short Circuit Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 4.5.4 Verifying Nested Loops . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 4.5.5 Verifier Run Time . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1314.6 Rewritable Loops . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133Architecture,4.6.1 Motivating Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 4.6.2 The Rewrite Map: ρ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135 4.6.3 Formulation of AVOps as Functions on the State . . . . . . . 136 4.6.4 Induced Rewrites and Rewriting AVOps . . . . . . . . . . . . . . . . 137 4.6.5 Short Circuit Theorem for Rewritable Loops . . . . . . . . . . . 138 4.6.6 Verifier Run Time on Rewritable Loops . . . . . . . . . . . . . . . . 140 4.6.7 Memory Requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1414.7 Extension to Full AVOp Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141 4.7.1 Extension of AVOp State and Hazard Checking . . . . . . . . 142 4.7.2 Extension of the Rewrite Map . . . . . . . . . . . . . . . . . . . . . . . . . . 145 4.7.3 Extension of Loops for Accessing Global Memory . . . . . . 146 4.7.4 Extension of Verification Algorithm . . . . . . . . . . . . . . . . . . . . . 1474.8 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 4.8.1 Restricted Global Memory Access for Verification . . . . . . 147 4.8.2 Stronger Short Circuit Theorem for Rewritable Loops . 148 4.8.3 Breaking up AVOp Streams to Increase AVOp FeedRate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148 4.8.4 Verifying the Verifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 4.8.5 Modifications for Cached Memory Multicore Processors 149 4.8.6 Scheduling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 4.8.7 Fault Tolerance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1504.9 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150Parallel computer architectures have now become almost universal, with even mobile phones containing dual core processors. Taking full advantage of the performance available in a computer system requires taking full advantage of the parallelism offered by that system. Opposed to the need for high performance is the need to verify the code’s requirements. Programming such architectures has long been recognized as a difficult task. Both requirements for performance and verifiability are difficult to attain.