 Timestamp:
 Sep 27, 2012, 5:46:59 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2363 r2364 138 138 139 139 The rest of this paper is a detailed description of our proof that is marginally still a work in progress. 140 \paragraph{Matita} 140 141 %  % 142 % SECTION % 143 %  % 144 \section{Matita} 145 \label{sect.matita} 141 146 Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. 142 147 It features dependent types that we exploit in the formalisation. … … 324 329 Conceptually the assembler works in two passes. 325 330 The first pass expands every pseudoinstruction into a list of machine code instructions using the function \texttt{expand\_pseudo\_instruction}. The policy 326 determines which expansion among the alternatives will be cho osedfor331 determines which expansion among the alternatives will be chosen for 327 332 pseudojumps and pseudocalls. Once the expansion is performed, the cost 328 333 of the pseudoinstruction is defined as the cost of the expansion. … … 376 381 still to be performed when expanding the instruction at \texttt{ppc}. 377 382 378 To solve the issue, we define the policy \texttt{policy} as a map s379 from a valid pseudo address to the corresponding address in the assembled383 To solve the issue, we define the policy \texttt{policy} as a map 384 from a valid pseudoaddress to the corresponding address in the assembled 380 385 program. 381 386 Therefore, $\delta$ in the example above can be computed simply as 382 \texttt{ sigma(a)  sigma(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that387 \texttt{policy(a)  policy(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that 383 388 $\delta < 128$. When this is not the case, the function emits an 384 389 \texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always … … 394 399 the sum of the size of all the expansions of the pseudoinstructions that 395 400 preceed the one at address \texttt{a}: the assembler just concatenates all 396 expansions one after another. To grant this property, we impose a401 expansions sequentially. To grant this property, we impose a 397 402 correctness criterion over policies. A policy is correct when for all 398 403 valid pseudoaddresses \texttt{ppc} … … 654 659 Not every proof has been carried out in this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way. 655 660 It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions. 656 %\paragraph{Related work} 657 661 \paragraph{Related work} 658 662 % piton 659 663 We are not the first to consider the correctness of an assembler for a nontrivial assembly language. … … 666 670 Care must be taken to ensure that the time properties of an assembly program are not modified by assembly lest we affect the semantics of any program employing the MCS51's I/O facilities. 667 671 This is only possible by inducing a cost model on the source code from the optimisation strategy and input program. 668 %\paragraph{Resources} 669 672 \paragraph{Resources} 670 673 Our source files are available at~\url{http://cerco.cs.unibo.it}. 671 674 We assumed several properties of `library functions', e.g. modular arithmetic and datastructure manipulation.
Note: See TracChangeset
for help on using the changeset viewer.