Abstract
The branch displacement problem is a well-known problem in assembler design. It revolves around the feature, present in several processor families, of having different instructions, of different sizes, for jumps of different displacements. The problem, which is provably NP-hard, is then to select the instructions such that one ends up with the smallest possible program.
During our research with the CerCo project on formally verifying a C compiler, we have implemented and proven correct an algorithm for this problem. In this paper, we discuss the problem, possible solutions, our specific solutions and the proofs.
Research supported by the CerCo project, within the Future and Emerging Technologies (FET) programme of the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number 243881.
Chapter PDF
Similar content being viewed by others
References
Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Automated Reasoning 39, 109–139 (2007)
Dickson, N.G.: A simple, linear-time algorithm for x86 jump encoding. CoRR abs/0812.4973 (2008)
Hyde, R.: Branch displacement optimisation (2006), http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3
Intel: Intel 64 and IA-32 Architectures Developer’s Manual, http://www.intel.com/content/www/us/en/processors/architectures-software-developer-manuals.html
Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43, 363–446 (2009), http://dx.doi.org/10.1007/s10817-009-9155-4 , doi: 10.1007/s10817-009-9155-4
Mulligan, D.P., Sacerdoti Coen, C.: On the correctness of an optimising assembler for the intel MCS-51 microprocessor. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 43–59. Springer, Heidelberg (2012), http://dx.doi.org/10.1007/978-3-642-35308-6_7
Robertson, E.L.: Code generation and storage allocation for machines with span-dependent instructions. ACM Trans. Program. Lang. Syst. 1(1), 71–83 (1979), http://doi.acm.org/10.1145/357062.357067
Small device C compiler 3.1.0 (2011), http://sdcc.sourceforge.net/
Szymanski, T.G.: Assembling code for machines with span-dependent instructions. Commun. ACM 21(4), 300–308 (1978), http://doi.acm.org/10.1145/359460.359474
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boender, J., Sacerdoti Coen, C. (2014). On the Correctness of a Branch Displacement Algorithm. In: Ábrahám, E., Havelund, K. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2014. Lecture Notes in Computer Science, vol 8413. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54862-8_53
Download citation
DOI: https://doi.org/10.1007/978-3-642-54862-8_53
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54861-1
Online ISBN: 978-3-642-54862-8
eBook Packages: Computer ScienceComputer Science (R0)