Abstract
Parallel programming is rapidly gaining importance as a vector to develop high performance applications that exploit the improved capabilities of modern computer architectures. In consequence, there is a need to develop analysis and verification methods for parallel programs.
Sequoia is a language designed to program parallel divide-and-conquer programs over a hierarchical, tree-structured, and explicitly managed memory. Using abstract interpretation, we develop a compositional proof system to analyze Sequoia programs and reason about them. Then, we show that common program optimizations transform provably correct Sequoia programs into provably correct Sequoia programs.
This work is partially supported by the EU project MOBIUS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alpern, B., Carter, L., Ferrante, J.: Modeling parallel computers as memory hierarchies. In: Proc. Programming Models for Massively Parallel Computers (1993)
Barthe, G., Grégoire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 301–317. Springer, Heidelberg (2006)
Barthe, G., Kunz, C.: Certificate translation in abstract interpretation. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 368–382. Springer, Heidelberg (2008)
Bornat, R., O’Hearn, P.W., Calcagno, C., Parkinson, M.: Permission accounting in separation logic. In: Principles of Programming Languages, pp. 259–270. ACM Press, New York (2005)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages, pp. 269–282 (1979)
Dally, W.J., Labonte, F., Das, A., Hanrahan, P., Ho Ahn, J., Gummaraju, J., Erez, M., Jayasena, N., Buck, I., Knight, T.J., Kapasi, U.J.: Merrimac: Supercomputing with streams. In: Conference on Supercomputing, p. 35. ACM, New York (2003)
Fatahalian, K., Horn, D.R., Knight, T.J., Leem, L., Houston, M., Park, J.Y., Erez, M., Ren, M., Aiken, A., Dally, W.J., Hanrahan, P.: Sequoia: programming the memory hierarchy. In: Conference on Supercomputing, p. 83. ACM Press, New York (2006)
Hermenegildo, M.V., Rossi, F.: Strict and nonstrict independent and-parallelism in logic programs: Correctness, efficiency, and compile-time conditions. J. Log. Program. 22(1), 1–45 (1995)
Houston, M., Young Park, J., Ren, M., Knight, T., Fatahalian, K., Aiken, A., Dally, W.J., Hanrahan, P.: A Portable Runtime Interface For Multi-Level Memory Hierarchies. In: Scott, M.L. (ed.) PPOPP, ACM, New York (2008)
Kapasi, U.J., Rixner, S., Dally, W.J., Khailany, B., Ho Ahn, J., Mattson, P.R., Owens, J.D.: Programmable stream processors. IEEE Computer 36(8), 54–62 (2003)
Knight, T.J., Young Park, J., Ren, M., Houston, M., Erez, M., Fatahalian, K., Aiken, A., Dally, W.J., Hanrahan, P.: Compilation for explicitly managed memory hierarchies. In: Yelick, K.A., Mellor-Crummey, J.M. (eds.) PPOPP, pp. 226–236. ACM, New York (2007)
Narayanasamy, S., Wang, Z., Tigani, J., Edwards, A., Calder, B.: Automatically classifying benign and harmful data races using replay analysis. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 22–31. ACM, New York (2007)
Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages, New York, NY, USA, pp. 106–119. ACM Press, New York (1997)
Necula, G.C., Lee, P.: Safe kernel extensions without run-time checking. In: Operating Systems Design and Implementation, Seattle, WA, October 1996, pp. 229–243. USENIX Assoc. (1996)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1-3), 271–307 (2007)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica Journal 6, 319–340 (1975)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, Copenhagen, Denmark, July 2002. IEEE Computer Society, Los Alamitos (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barthe, G., Kunz, C., Sacchini, J.L. (2008). Certified Reasoning in Memory Hierarchies. In: Ramalingam, G. (eds) Programming Languages and Systems. APLAS 2008. Lecture Notes in Computer Science, vol 5356. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89330-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-89330-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89329-5
Online ISBN: 978-3-540-89330-1
eBook Packages: Computer ScienceComputer Science (R0)