On the correctness of a branch displacement algorithm

Book chapter

Boender, J. and Sacerdoti Coen, C. 2014. On the correctness of a branch displacement algorithm. in: Ábrahám, E. and Havelund, K. (ed.) Tools and Algorithms for the Construction and Analysis of Systems : 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings Springer.
Chapter titleOn the correctness of a branch displacement algorithm
AuthorsBoender, J. and Sacerdoti Coen, C.
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.

Keywordsformal verification; interactive theorem proving; assembler; branch displacement optimisation
Research GroupArtificial Intelligence group
Foundations of Computing group
Book titleTools and Algorithms for the Construction and Analysis of Systems : 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings
EditorsÁbrahám, E. and Havelund, K.
PublisherSpringer
SeriesLecture Notes in Computer Science
ISBN
Hardcover9783642548611
ISSN0302-9743
Publication dates
Print24 Mar 2014
Publication process dates
Deposited05 Sep 2014
Output statusPublished
Accepted author manuscript
Copyright Statement

Archiving permitted by publisher but embargoed for 12 months from date of publication.

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-642-54862-8_53
LanguageEnglish
JournalLecture Notes in Computer Science
Permalink -

https://repository.mdx.ac.uk/item/84x2w

Log in to edit

Download files

Accepted author manuscript
merged_document.pdf

  • 26
    total views
  • 7
    total downloads
  • 1
    views this month
  • 2
    downloads this month

Export as