A fast verified liveness analysis in SSA form. (English) Zbl 07614679
Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12167, 324-340 (2020).
Summary: Liveness analysis is a standard compiler analysis, enabling several optimizations such as deadcode elimination. The SSA form is a popular compiler intermediate language allowing for simple and fast optimizations. Boissinot et al. [7] designed a fast liveness analysis by combining the specific properties of SSA with graph-theoretic ideas such as depth-first search and dominance. We formalize their approach in the Coq proof assistant, inside the CompCertSSA verified C compiler. We also compare experimentally this approach on CompCert’s benchmarks with respect to the classic data-flow-based liveness analysis, and observe performance gains.
For the entire collection see [Zbl 1498.68017].
For the entire collection see [Zbl 1498.68017].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Companion website. http://www.irisa.fr/celtique/ext/fast_liveness/ |
| [2] | Appel, A.W., Palsberg, J.: Modern Compiler Implementation in Java, 2nd edn. Cambridge University Press, Cambridge (2002) · Zbl 1058.68035 · doi:10.1017/CBO9780511811432 |
| [3] | Barthe, G., Demange, D., Pichardie, D.: Formal verification of an SSA-based middle-end for CompCert. ACM Trans. Program. Lang. Syst. 36(1), 4:1-4:35 (2014). https://doi.org/10.1145/2579080 · doi:10.1145/2579080 |
| [4] | Blazy, S., Demange, D., Pichardie, D.: Validating dominator trees for a fast, verified dominance test. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 84-99. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_6 · Zbl 1466.68030 · doi:10.1007/978-3-319-22102-1_6 |
| [5] | Boissinot, B., Brandner, F., Darte, A., de Dinechin, B.D., Rastello, F.: A non-iterative data-flow algorithm for computing liveness sets in strict SSA programs. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 137-154. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25318-8_13 · doi:10.1007/978-3-642-25318-8_13 |
| [6] | Boissinot, B., Darte, A., Rastello, F., de Dinechin, B.D., Guillon, C.: Revisiting out-of-SSA translation for correctness, code quality and efficiency. In: Proceedings of the CGO 2009, The Seventh International Symposium on Code Generation and Optimization, Seattle, Washington, USA, 22-25 March 2009, pp. 114-125. IEEE Computer Society (2009). https://doi.org/10.1109/CGO.2009.19 |
| [7] | Boissinot, B., Hack, S., Grund, D., de Dinechin, B.D., Rastello, F.: Fast liveness checking for SSA-form programs. In: Soffa, M.L., Duesterwald, E. (eds.) Sixth International Symposium on Code Generation and Optimization (CGO 2008), 5-9 April 2008, Boston, MA, USA, pp. 35-44. ACM (2008). https://doi.org/10.1145/1356058.1356064 |
| [8] | Das, D., de Dinechin, B.D., Upadrasta, R.: Efficient liveness computation using merge sets and DJ-graphs. TACO 8(4), 27:1-27:18 (2012). https://doi.org/10.1145/2086696.2086706 · doi:10.1145/2086696.2086706 |
| [9] | Demange, D., de Retana, Y.F.: Mechanizing conventional SSA for a verified destruction with coalescing. In: Zaks, A., Hermenegildo, M.V. (eds.) Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, 12-18 March 2016, pp. 77-87. ACM (2016). https://doi.org/10.1145/2892208.2892222 |
| [10] | Georgiadis, L., Tarjan, R.E.: Dominator tree certification and divergent spanning trees. ACM Trans. Algorithms 12(1), 11:1-11:42 (2016). https://doi.org/10.1145/2764913 · Zbl 1398.68396 · doi:10.1145/2764913 |
| [11] | Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE/ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA, pp. 75-88. IEEE Computer Society (2004). https://doi.org/10.1109/CGO.2004.1281665 |
| [12] | Leroy, X.: A formally verified compiler back-end. J. Autom. Reasoning 43(4), 363-446 (2009). https://doi.org/10.1007/s10817-009-9155-4 · Zbl 1185.68215 · doi:10.1007/s10817-009-9155-4 |
| [13] | Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: ERTS 2016: Embedded Real Time Software and Systems. SEE (2016) |
| [14] | Ramalingam, G.: On loops, dominators, and dominance frontiers. ACM Trans. Program. Lang. Syst. 24(5), 455-490 (2002). https://doi.org/10.1145/570886.570887 · doi:10.1145/570886.570887 |
| [15] | Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A.C.J., Owens, S., Norrish, M.: The verified CakeML compiler backend. J. Funct. Program. 29, e2 (2019). https://doi.org/10.1017/S0956796818000229 · Zbl 1493.68091 · doi:10.1017/S0956796818000229 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
