 Timestamp:
 Jun 15, 2012, 1:17:15 AM (9 years ago)
 Location:
 src/ASM/CPP2012policy
 Files:

 1 added
 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/conclusion.tex
r2064 r2084 1 1 \section{Conclusion} 2 3 In the previous sections, we have discussed the branch displacement optimisation 4 problem, presented an optimised solution, and discussed the proof of 5 termination and correctness for this algorithm, as formalised in Matita. 6 7 \subsection{Related work} 8 9 As far as we are aware, this is the first formal discussion of the branch 10 displacement algorithm. 11 12 (Piton? CompCert?) 13 14 \subsection{Formal development} 15 16 All Matita files related to this development can be found on the CerCo 17 website, \url{http://cerco.cs.unibo.it}. The specific part that contains the 18 branch displacement algorithm is in the {\tt ASM} subdirectory, in the files 19 whose name starts with {\tt Policy}. 
src/ASM/CPP2012policy/main.tex
r2064 r2084 4 4 \usepackage{amsfonts} 5 5 \usepackage[british]{babel} 6 \usepackage{hyperref} 6 7 \usepackage[utf8]{inputenc} 7 8 \usepackage{listings} … … 14 15 15 16 \mainmatter 16 \title{On the correctness of a branch displacement algorithm }17 \title{On the correctness of a branch displacement algorithm\thanks{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 FETOpen grant number 243881}} 17 18 \author{Jaap Boender \and Claudio Sacerdoti Coen} 18 \institute{ Alma Mater StudiorumUniversità degli Studi di Bologna}19 \institute{Dipartimento di Scienze dell'Informazione, Università degli Studi di Bologna} 19 20 20 21 \maketitle … … 41 42 42 43 \bibliography{biblio} 43 \bibliographystyle{ plain}44 \bibliographystyle{splncs03} 44 45 45 46 \end{document} 
src/ASM/CPP2012policy/proof.tex
r2082 r2084 309 309 program size. Here, we only need {\tt out\_of\_program\_none}, 310 310 {\tt sigma\_compact} and the fact that $\sigma(0) = 0$. 311 312 Termination can now be proven through the fact that there is a $k \leq 2n$, with 313 $n$ the length of the program, such that iteration $k$ is equal to iteration 314 $k+1$. There are two possibilities: either there is a $k < 2n$ such that this 315 property holds, or every iteration up to $2n$ is different. In the latter case, 316 since the only changes between the iterations can be from shorter jumps to 317 longer jumps, in iteration $2n$ every jump must be long. In this case, 318 iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached.
Note: See TracChangeset
for help on using the changeset viewer.