On the correctness of a branch displacement algorithm

Part of book or chapter of book, Preprint English OPEN
Boender, Jaap ; Sacerdoti Coen, Claudio (2014)
  • Publisher: Springer
  • Related identifiers: doi: 10.1007/978-3-642-54862-8_53
  • Subject: Computer Science - Logic in Computer Science | Computer Science - Software Engineering

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.\ud \ud 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.
  • References (9)

    1. Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Automated Reasoning 39, 109{139 (2007)

    2. Dickson, N.G.: A simple, linear-time algorithm for x86 jump encoding. CoRR abs/0812.4973 (2008)

    3. Hyde, R.: Branch displacement optimisation. http://groups.google.com/group/ alt.lang.asm/msg/d31192d442accad3 (2006)

    4. Intel: Intel 64 and IA-32 Architectures Developer's Manual. http://www.intel.com/content/www/us/en/processors/ architectures-software-developer-manuals.html

    5. Leroy, X.: A formally veri ed compiler back-end. Journal of Automated Reasoning 43, 363{446 (2009), http://dx.doi.org/10.1007/s10817-009-9155-4, 10.1007/s10817-009-9155-4

    6. 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.) Certi ed Programs and Proofs, Lecture Notes in Computer Science, vol. 7679, pp. 43{59. Springer Berlin Heidelberg (2012), http://dx.doi.org/10.1007/978-3-642-35308-6_7

    7. Robertson, E.L.: Code generation and storage allocation for machines with spandependent instructions. ACM Trans. Program. Lang. Syst. 1(1), 71{83 (Jan 1979), http://doi.acm.org/10.1145/357062.357067

    8. Small device C compiler 3.1.0. http://sdcc.sourceforge.net/ (2011)

    9. Szymanski, T.G.: Assembling code for machines with span-dependent instructions. Commun. ACM 21(4), 300{308 (Apr 1978), http://doi.acm.org/10.1145/359460. 359474

  • Metrics
    No metrics available
Share - Bookmark