REALISTIC CORRECT SYSTEMS IMPLEMENTATION

The present article and the forthcoming second part on Trusted Compiler Implementation address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we ask: Can informaticians righteously be accounted for incorrectness of...

Повний опис

Збережено в:

Бібліографічні деталі
Дата:	2015
Автор:	Goerigk, W.
Формат:	Стаття
Мова:	English
Опубліковано:	PROBLEMS IN PROGRAMMING 2015
Теми:
Онлайн доступ:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/3
Теги:	Додати тег Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:	Problems in programming
Завантажити файл:

Репозитарії

Problems in programming

id	pp_isofts_kiev_ua-article-3
record_format	ojs
resource_txt_mv	ppisoftskievua/6e/5edaaab261b0b7d0c5f046b8f5a8ee6e.pdf
spelling	pp_isofts_kiev_ua-article-32018-09-26T13:18:29Z REALISTIC CORRECT SYSTEMS IMPLEMENTATION Goerigk, W. The present article and the forthcoming second part on Trusted Compiler Implementation address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we ask: Can informaticians righteously be accounted for incorrectness of systems, will they be able to justify systems to work correctly as intended? We understand the word justification in the sense: design of computer based systems, formulation of mathematical models of information flows, and construction of controlling software are to be such that the expected system effects, the absence of internal failures, and the robustness towards misuses and malicious external attacks are foreseeable as logical consequences of the models. PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2015-06-12 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/3 PROBLEMS IN PROGRAMMING; No 1 (2003) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2003) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2003) 1727-4907 en https://pp.isofts.kiev.ua/index.php/ojs1/article/view/3/5 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ
institution	Problems in programming
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date	2018-09-26T13:18:29Z
collection	OJS
language	English
topic
spellingShingle	Goerigk, W. REALISTIC CORRECT SYSTEMS IMPLEMENTATION
topic_facet
format	Article
author	Goerigk, W.
author_facet	Goerigk, W.
author_sort	Goerigk, W.
title	REALISTIC CORRECT SYSTEMS IMPLEMENTATION
title_short	REALISTIC CORRECT SYSTEMS IMPLEMENTATION
title_full	REALISTIC CORRECT SYSTEMS IMPLEMENTATION
title_fullStr	REALISTIC CORRECT SYSTEMS IMPLEMENTATION
title_full_unstemmed	REALISTIC CORRECT SYSTEMS IMPLEMENTATION
title_sort	realistic correct systems implementation
description	The present article and the forthcoming second part on Trusted Compiler Implementation address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we ask: Can informaticians righteously be accounted for incorrectness of systems, will they be able to justify systems to work correctly as intended? We understand the word justification in the sense: design of computer based systems, formulation of mathematical models of information flows, and construction of controlling software are to be such that the expected system effects, the absence of internal failures, and the robustness towards misuses and malicious external attacks are foreseeable as logical consequences of the models.
publisher	PROBLEMS IN PROGRAMMING
publishDate	2015
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/3
work_keys_str_mv	AT goerigkw realisticcorrectsystemsimplementation
first_indexed	2025-07-17T10:05:23Z
last_indexed	2025-07-17T10:05:23Z
_version_	1850413091109470208
fulltext	Теоретические и методологические основы программирования © Wolfgang Goerigk, Hans Langmaack, 2003 ISSN 1727-4907. Проблемы программирования. 2003. № 1 3 UDC 681.3.51 Wolfgang Goerigk, Hans Langmaack REALISTIC CORRECT SYSTEMS IMPLEMENTATION The present article and the forthcoming second part on Trusted Compiler Implementa- tion address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we ask: Can informaticians righteously be accounted for incorrectness of systems, will they be able to justify systems to work correctly as intended? We understand the word justification in the sense: design of computer based systems, formulation of mathematical models of information flows, and construction of controlling software are to be such that the expected system effects, the absence of internal failures, and the robustness towards misuses and malicious external at- tacks are foreseeable as logical consequences of the models. Since more than 40 years, theoretical informatics, software engineering and compiler construction have made important contributions to correct specification and also to correct high-level implementation of compilers. But the third step, translation - bootstrapping - of high level compiler programs to host machine code by existing host compilers, is as impor- tant. So far there are no realistic recipes to close this correctness gap, although it is known for some years that trust in executable code can dangerously be compromised by Trojan Horses in compiler executables, even if they pass strongest tests. In the present first article we will give a comprehensive motivation and develop a mathematical theory in order to conscientiously prove the correctness of an initial fully trusted compiler executable. The task will be modularized in three steps. The third step of machine level compiler implementation verification is the topic of the forthcoming second part on Trusted Compiler Implementation. It closes the implementation gap, not only for compilers but also for correct software-based systems in general. Thus, the two articles to- gether give a rather confident answer to the question raised in the title. 1. Introduction Users of computer based systems are often heavily annoyed by errors, fail- ures and system crashes. In our every day experience using programs we observe them to fail, for instance due to lack of memory, programming errors, compiler bugs, or misuses of optimizing compilers under wrong assumptions. Although very annoying, we all live with software errors, but we still hope that application pro- grammers, compiler constructors, operat- ing system designers and hardware engi- neers have at least been sensible enough to detect and to signal any such error. Undetected errors might have harmful consequences, in particular if they are intentional, perhaps due to viruses or Trojan Horses. Often the user is accountable, us- ing systems outside their specified do- mains without even reading manuals or documentation. However, a large number of system misbehaviors is still due to the system constructors themselves, to pro- fessionals, computer scientists, informati- cians. It is obvious that they should take responsibility as any professional has to. But software constructors and their com- panies hardly ever give guarantees for their products. And they are not even en- forced to because customers purchase software products in full awareness of de- fects. Nevertheless, informatics scientists and producers of computer based systems are responsible and not allowed to per- manently neglect the problem of system misbehaviors in practice. 1.1. Motivation and Outline. Our article addresses correct construction and functioning of large computer based sys- tems. In view of so many annoying and dangerous system misbehaviors we ask (and positively answer) the question: Can informaticians be righteously accounted for system weaknesses, will they be able to justify systems to work correctly as in- tended, to be dependable, reliable, robust? Since hardware turns out to be quite reliable, the question comes down to software, i.e. to abstract and mathe- matically treatable components of sys- tems. The rigid nature of matter educates hardware technologists to be extremely sensitive towards hardware failures; they Теоретические и методологические основы программирования 4 are felt as sensations. So system faults are mostly and increasingly caused by soft- ware. This observation is crucial and matches the clear delimitation of respon- sibilities between hardware and system software engineering. Software engineers are permitted to assume hardware to work correctly, and to exploit this assumption for equally sensitive, rigorous low level implementation verification of software. Once software engineers and application programmers can count on (trust in) the correctness of their low level machine implementations and integrated systems, an equal status of sensitivity also for software faults becomes justifiable. That is to say, at the low end, sys- tem software engineering meets hardware engineering, and at the upper end, com- piler constructors and system software engineers meet application programmers and software engineers. They want to ex- press their software in problem-oriented languages and rely on machine inde- pendent semantics. Compiler constructors cannot be made responsible for applica- tion program faults. Actually, a compiler has to be constructed without any knowl- edge about the intended meaning of ap- plication programs. The contract has to be with respect to program semantics. As a return, the application programmer ex- pects correctly implemented machine ex- ecutables. But both, application and sys- tem programmers have to be aware of what kinds of implementation correct- nesses make sense and can realistically be guaranteed. We will reflect realistic requirements and introduce the notion of relative correctness and its preservation and variants in view of data and program representation and of errors which can be accepted or others which have to be avoided. Although an area of research and development since 40 years, realistic lan- guage implementation, a central topic in system software engineering, is still a se- vere gap in trustworthiness. Practical compiler construction proceeds in three steps: (1) Specification of a compiling re- lation from source language to target machine code, (2) implementation of the compiling relation as a compiler program in an appropriate high level system pro- gramming language, and (3) boot- strapping the compiler, i.e. translation of the compiler source program into host machine code using an existing host compiler. Theoretical informatics, soft- ware engineering and compiler construc- tion have importantly contributed to- wards correctness of the first two steps. 1.1.1. Trusted Compiler Imple- mentation. But how to verify the third, the low level step? So far there are no realistic recipes to close this gap, al- though it is known for many years (at least since Ken Thompson's Turing Award lecture in 1984) that trust in ex- ecutable code can dangerously be com- promised by Trojan Horses in compiler executables, even if they pass strongest tests. Our article will show how to close this low level gap. The Deutsche For- schungsgemeinschaft (DFG) research group Verifix has developed the method of rigorous syntactic a-posteriori code in- spection in order to remove every source of crucial faults in initial compilers for appropriate high level system program- ming languages. The method employs multi-pass translation with tightly neighboring intermediate languages and a diagonal bootstrapping technique which effectively is based on the above mentioned correctness assumptions and deliberations. A-posteriori result checking is applicable for the construction of veri- fied compiler generators as well, and it is crucial to the development of strategies to substitute existing system software by proved correct modifications. There is a current trend for system software to be required open source, enabling source code scrutiny for operat- ing system components, networking soft- ware and also for compilers and other tools and utilities. This will definitely un- veal a lot of bugs and even malicious code like Trojan Horses or so-called easter eggs. However, we want to stress, that the open source idea crucially de- pends on trusted compilation. Source level scrutiny does not sufficiently guar- antee trustworthiness of executable soft- Теоретические и методологические основы программирования 5 ware [Thompson84, Goerigk99b, Goe- rigk00a, Goerigk00b]. There are sophisti- cated and intelligent techniques to com- pletely hide Trojan Horses in binary compiler executables, which are not part of the alleged source code, but might cause unexpected, arbitrary, even catas- trophic effects if target programs are eventually executed. No source code scrutiny, no source level verification, no compiler validation, virtually no test, not even the strong compiler bootstrap test does help. Note that in this situation it is also very unlikely that any of the known security techniques will help, because not even the application programmer can give a guarantee that her/his delivered application has not been compromised by auxiliary software utilities or compilers used during software construction. Industrial software production for realistic safety and security critical appli- cations enforces immense checking ef- forts. The amount of work is apparently unmanageable, and consequently, it is left undone. That is to say: On the one hand, we observe dangerous omissions in industrial practice. On the other hand, we realize how enormous the problems are. Thus, informatics science, in particular viewed at as an engineering science, has to attack them as problems of basic re- search – supported by research funding institutions like Deutsche Forschungsge- meinschaft (DFG) or German Federal Board of Safety and Security in Informa- tion Technology (Bundesamt für Sicher- heit in der Informationstechnik, BSI), in- stitutions which we find in all states with high science and technology standards. We are not allowed to leave industry people alone with their responsibility for necessary efforts which are seemingly unsurmountable at present. It is neces- sary to clearly identify the problems and to work towards methods for their rigor- ous solution which work out in practice. Mathematics as the classical structure science helps. Again and again, mathe- maticians invent ways of gaining and communicating insights, which are rigor- ous and convincing even though or maybe even because they are not com- pletely formal. We shall see that in the central area of correct compiler construc- tion and implementation our techniques of insight can cope with realistic software tasks, and of course then can serve as a model outside the area of compilers. Ac- tually, it is the too often neglected low level implementation verification of so- called initial compilers which involves a certain amount of manual checking and proving [Goerigk/Langmaack01b]. For principle reasons we cannot leave all checking work to programmed computers if we do not want to run into circuli vitiosi. Trust in any executed program would furtheron dangerously and hope- lessly depend on auxiliary software of uncertain pedigree [HSE01]. We do not want to blame or con- demn anybody personally. The problem is enormous, very awkward, and in certain central areas it seems nearly unreasonable to ask for problem solutions in depth. However, because of potential disastrous consequences, informaticians must attack the problem and seek for solutions to give rigorous guarantees. And we shall see that in the crucial area of correct compiler construction, informatics sci- ence can achieve quite a lot. There is a remarkable interplay of informatics as a foundational structure science and as an engineering science. The realistic recipe of bootstrap- ping and syntactical a-posteriori code in- spection, which Verifix has developed in order to close the low level implementa- tion gap rigorously, and which has been applied to a realistic compiler executable for a useful systems programming lan- guage, is the topic of the second article on Trusted Compiler Implementation [Go- erigk/Langmaack01b]. 1.2. Notions Mentioned in the Title. Let us briefly explain the notions which we mentioned in the title of this essay: Informatics (Computer Science in the Anglo-American literature) is the sci- entific discipline of design, construction and networking and of application and programming of computers (often called processors). Although not the most mod- ern one, this definition is well stressing Теоретические и методологические основы программирования 6 the two important areas of work: hard- ware and software. Computer based sys- tems (CBS) are engineering systems with embedded computers, programs, sensors, actuators, clocks and connecting chan- nels in a physical environment [Schwei- zer/Voss96]. Realistic computer based systems use to be large, complex, and safety and/or security critical [Laprie94]. The latter means that systems may cause heavy damages to health and economy by unintended (internal) failures and by intended (external) attacks. As a matter of fact, the bare exis- tence of large computer based systems is justified. We need them. But what about correct construction and functioning of such systems? Can informaticians be made responsible, be accounted for, will they be able to justify systems to work correctly as intended? We use the term justification in this sense, i.e. for the de- sign of computer based systems, the for- mulation of mathematical models of in- formation flows in systems and the con- struction of software to be such that the expected system effects and the absence of failures and violations are foreseeable as logical consequences of the models alone. Not every system has such sub- stantial delineable area which can be jus- tified in this rigorous sense. In our opin- ion, however, if such a rigorous treatment is possible, it should be required for high safety and security standards. If we can logically foresee (infer) every desired property, especially safety and security properties, then we say that the computer based system has been (mathematically) proved correct, has been verified. We use the word verification in this sense, whereas validation means finding by ex- periments that a system fulfills our in- tents. Validation is not our main topic in this essay. 1.3. Consistent Checkability of Software Production Processes. Large computer based systems are essentially controlled by embedded processors and their software. General experience shows that the hardware processors actually work by far more reliably than software does and, hence, the weaknesses of com- puter based systems are in most cases due to software problems. Every software production (implementation) process to- day still has two major gaps in trustwor- thiness of consistent checkability, namely the transitions from 1. software design to high level source code (high level software engi- neering) and 2. from high level code to inte- grated executable binary machine code (realistic compilation). Both gaps are under investigation in research and development since more than 30 years, but nevertheless even real- istic compilation is still a severe gap in trustworthiness [BSI96]. Strictly speaking, realistic compilers are not correct and no compiler has yet sufficiently been veri- fied. So the question arises whether in- formatics and in particular theoretical computer science, programming language theory, compiler construction and soft- ware engineering do not have any useful results to help in this situation. They have. And the insights are deep and also practical. But we have to admit that the results are often depending on too many complicated assumptions which the prac- tical user has to check for in realistic situations. And unfortunately, in practice this so far requires many properly edu- cated engineers and a lot of mathemati- cal and logical skill. If we seriously look at informatics also as an engineering science, we ought to demonstrate solutions and to show that the necessary checking can be done in a thorough and convincing way. In particu- lar, in this essay we will demonstrate a strategic solution to close the second gap, that of correct realistic compilation, which in turn is necessary for a convinc- ing high level software engineering. 1.4. DFG-Research Project Verifix- Correct Compilers. Correct realistic compilation is the major goal of the German joint project Verifix on Correct Compilers of the universities of Karlsruhe (G. Goos, W. Zimmermann), Kiel (W. Goerigk, H. Langmaack) and Ulm (A. Dold, F.W. von Henke). Verifix is a DFG- funded research group since 1996. The goal is to develop repeatable engineering Теоретические и методологические основы программирования 7 repeatable engineering methods for con- structing correct compilers and compiler generators • for realistic, industrially applica- ble imperative and object-oriented source programming languages and • real world target and host proc- essors • which, by help of mechanical proof support (e.g. by PVS [Owre+92] or ACL2 [Kaufmann/Moore94]) and by ex- ploiting the idea of a-posteriori result checking are rigorously verified as execu- table host machine programs and • which nevertheless generate ef- ficient code that compares to unverified compilers. • Verifix uses practically and in- dustrially approved compiler construction methods • and the proof methodology sup- plements compiler construction, not vice versa. Compiler construction is crucial to the construction of (large) computer based systems, and correct realistic com- pilers are necessary for a convincing con- struction process of correctly working systems. Systems consist of hardware and controlling software, and software splits in system and application software. Com- piler programs are system software, and even compilers like any other piece of systems or applications are executable by compiling into binary processor code. There is no doubt that it is reasonable to require compiling to be correct. Fig 1. The central role of correct compilers Sometimes we use the termini fully correct or fully verified if we want to em- phasize that not only a mathematically specified compiling relation CSL TL between source language SL and target language TL is proved correct, but that also an ex- ecutable compiler version implementing this relation and implemented in binary HML-machine code of a real world host processor HM is proved correct without depending on any auxiliary unchecked tool execution. Note that the term fully correct makes sense for arbitrary software as well, which is mathematically specified on the one hand, and implemented on a machine on the other. We will make a difference between the terms proved correct and provably correct. We use provably correct in order to indicate that we are interested to de- velop methods which generate proof documents, often aided by computers. These documents can rigorously be checked to be proofs1. If the documents are checked, for instance for a concrete compiler, we use the term proved correct. Of course, we have to admit that check- ing might bear errors. So proved does not claim absolute truth. But it claims a rig- orous attempt to gain mathematical cer- tainty, which is much more than many other research areas can achieve. It is not true, that investigation into correct realistic compilation does not pay off just because software design and high level software engineering probably show up many more faults than compila- tion. Unless we close the lower level gap with mathematical certainty, a major goal of Verifix, potential incorrect compilation will always critically disturb the recogni- tion of certainties resp. uncertainties in high level software engineering. Correct realistic compilation establishes a trust- worthy execution basis for further soft- ware development. Informatics is well responsible for compilers with their program semantics and machines. Full verification of com- pilers is manageable and feasible. Com- pared to programming language theory and compiler construction practice, no other discipline of practical computer science is so well equipped with theory. Investigations in Verifix have brought up ideas and methods to incrementally re- place compilers and to replace or encap- 1 by more or less skilled informaticians. The required skill varies. Not every checking work requires trained mathematicians or logicians. Теоретические и методологические основы программирования 8 sulate system software components by fully verified software. 1.5. Levels of Trustworthiness and Quality. The lower level gap due to real- istic compilation has been made public by governmental boards like the German BSI, but also in other countries. In 1989, BSI published IT-safety and security lev- els (of trustworthiness or IT-quality) [ZSI89]. In Germany, there are eight lev- els from Q0 (unsufficiently checked) up to Q7 (formally verified, proofs and im- plementation are performed by officially admitted tools). However, an "officially admitted" tool (like a compiler or theorem prover) is not necessarily fully verified. So for in- stance a compiler just needs to pass an official validation test suite. It is well- known, that such tests do not suffice nor replace correctness proofs [Dijkstra76]. Official IT-certification prescriptions like those published by BSI in 1989/90/94 [ZSI89, ZSI90, BSI94] require: "The compilers employed must be offi- cially validated and be admitted as implementation tools for Q7-systems by an official evaluation board." The terminus validated reveals that for tools like compilers the evaluation boards at present can only validate for instance by applying official test suites. The boards do not see any other rigorous checking or proof technique and hence suspect that one is not allowed to trust in the correctness of generated machine code and hence of any compiler. Thus, consequently BSI added the following additional requirement: “The transformations from source to target code executed by a compiler program on a host machine must be a- posteriori checkable (“nachvollzieh- bar”, “inspectable”).” For this reason certification au- thorities still do not trust in any existing realistic compiler. Instead, they often per- form parallel semantical inspections of both high level code and low level ma- chine code [Pofahl95], i.e. they check a- posteriori that the target code will work as expected from the source code. Such a code-inspection is a rigor- ous a-posteriori checking of the target program πTL to perform as expected from the source program πSL, where the target program is the result of a successful compilation of the (well-formed) source program. The hope is that this is feasible if the mapping CSL TL (the specification of the transformation) from source to target programs is “inspectable”, and hence that it is sufficient to check (πSL, πTL) ∈ CSL TL. However, as long as CSL TL is not proved correct, the checking involves semantical considerations. Inspection resp. a-posteriori result checking is an old idea [Blum+89]. And we know the method from school mathematics: since for instance integer division is felt more error prone than multiplication, we double-check the re- sults of division by multiplication. We also use to double-check the results of linear equations solutions by simpler ma- trix-vector-multiplication. By code inspec- tion with respect to compilers we mean the a-posteriori result checking of com- piler generated code. Result checking is often much easier than (a-posteriori) veri- fication. Moreover, it is an interesting ob- servation, that industrial software engi- neers and certification boards trust the technique of a-posteriori result checking. Although there is a well-established and reasonably developed program verifica- tion theory, it is often not well-applicable to large systems or even large amounts of low level code. Therefore it is so interest- ing to observe, both from a theoretical and from a practical point of view, that realistic scientifically founded fully veri- fied compiler construction has to reach back also to a-posteriori checking to a small, but decisive extent. We will see this later while proving low level compiler implementation correctness [Goerigk/Langmaack01b] and hence full compiler correctness. Conse- quently, since this is possible and feasi- ble, already in 1989/90 one of the authors proposed to introduce an even higher IT- safety and security level of quality Q8 Теоретические и методологические основы программирования 9 (Production, proof and checking tools are fully verified, not only at high level, but also down to implementations in execu- table binary machine code). Otherwise, the low level gap of realistic compilation will remain open forever. 2. Code Inspection in Compiler Con- struction Processes The Verifix-thesis is that after 40 years compiler construction and more than 30 years software engineering it should no longer be necessary to inspect low level generated code, not even for safety and security critical software. The new higher quality level Q8 should be introduced which is reaching beyond Q7. It should be desirable and required for industrial software construction, in par- ticular for realistic compilers. We cannot entirely avoid manual low level code in- spection [Fagan86], however, it is only necessary for initial compiler executables which cannot be implemented on behalf of a verified bootstrapping compiler ex- ecutable. The requirement for low level code inspection only make sense in this respect. In principle, it should suffice to perform this work exactly once. However, realistic industrial correct compiler engi- neering additionally needs repeatable methods for constructing correct initial compiler implementations from the scratch whenever necessary. The goal of correct realistic com- piler construction in the view of Verifix is that compiler executables on real world host machines have to be provably cor- rect, and if they are to be used for safety and security critical software implementa- tion, they have to be proved correct. That means, that any executable binary ma- chine program successfully generated from a well-formed source program is provably or proved correct with respect to the source program semantics. Ma- chine program correctness may only de- pend on • the correctness of source level application programs with respect to their specifications, • hardware, i.e. target and host processors to work correctly as described in their instruction manuals, • correct rigorous (mathematical, logical) reasoning Application programmers are re- sponsible for the first assumption and hardware designers for the second. Hence, the compiler constructor only needs con- sider the semantics of well-formed source programs and processors and needs not respect any further intention of system or application programmers. Since correctness of a compiler is defined by correctness of ist resulting target programs, we only depend on this property which equally well can be estab- lished by a-posteriori result checking. In that case we sometimes use the term veri- fying compiler. Suppose we have a given unverified compiler τHL from SL to TL written (or generated) in some high level host programming language HL. Suppose that τHL compiles via intermediate lan- guages SL = IL0, IL1, ..., ILm = TL, m ≥ 1, by compiler passes τ1 HL; τ2 HL; ...; τm HL = τHL which for a well-formed source program πSL may successfully generate intermedi- ate programs πSL = πIL0, πIL1, ..., πILm = πTL. For all passes τi HL we assume that we are able to write a-posteriori code in- spection procedures γi HL which we insert into τHL: τ1 HL; γ1 HL; τ2 HL; γ2 HL; ...; τm HL; γm HL = τ´HL. Syntax and static semantics of τHL has to make sure that the unverified passes τi HL are safely encapsulated such that their semantics cannot interfere with the inspection procedures nor with any other passes. This method is obviously relying on the existence of an initial cor- rect and correctly implemented compiler from HL to the compiler host machine code, because it is by no means realistic to assume HL to be a binary machine language. Теоретические и методологические основы программирования 10 In practice, there is no way around an initial correct compiler executable on some host machine. Moreover, HL should at least be usable, if not comfortably us- able, for systems programming and writ- ing compilers. Since programming languages, their semantics, hardware processors and their binary machine codes can accep- tedly be modeled using mathematics, correct compiler specification and im- plementation are in principle mathemati- cal tasks. Perhaps they are not that deep, however, they require an exorbitant or- ganization which is to be convincing and without any logical gap. Hardware engineering has, for good money reasons, developed an error handling culture by far better than soft- ware engineering [Goerke96]. Hardware errors are sensations, whereas software errors are commonplace. Since hardware errors cannot easily be repaired, they bear the risk of high economic damage. Thus, hardware engineers seek even for small gaps where faults could creep in. Seemingly, software errors can easily be repaired. But often bug fixes make things even worse, and also software errors bear a high risk. If we assume hardware correct, then we can rely on hardware processors programmed by correct and correctly im- plemented software. However, if a proc- essor is endowed with verified high level programs, but additionally with some non-verified compilers, then it generally will not work failure-free for the time be- ing. But the goal of fully reliable systems software is not hopeless. We will come back to this. 3. Related Work on Compiler Verification Let us ask if literature does help in order to prove the three compiler imple- mentation steps correct. Actually, we find intensive work on steps 1 and 2, although often under unrealistic assumptions so that the results have to be handled with care. Step 3 has nearly totally been ne- glected. If the phrase ``compiler verifica- tion´´ is used, then most of the authors mean step 1. There is virtually no work on full compiler verification. Therefore, the ProCoS project (1989—1995) has made a clear distinction between compil- ing verification (step 1) and compiler im- plementation verification (steps 2 and 3). Compiling verification is part of theoretical informatics and program se- mantics and work on it has been started by J. McCarthy and J.A. Painter in 1967 [McCarthy/Painter67]. Proof styles are operational [McCarthy/Painter67, Boer- ger/Rosenzweig92, Boerger/Schulte98] or denotational [Milne/Strachey76] depend- ing on how source language semantics is defined. If a source language has loops or (function) procedures, then term rewriting or copy rule semantics is employed throughout [Langmaack73, Loeckx/Sie- be87]. Other operational styles split in natural [Nielson/Nielson92] or structural [Plotkin81] operational or state-machine- like [Gurevich91, Gurevich95]. Denota- tional semantics has started with D. Scott's work [Scott70, Scott/Strachey71], and typical compiling correctness proofs can be found in [Milne/Strachey76]. The au- thors in [Hoare+93, Sampaio93, Mueller- Olm96, Mueller-Olm/Wolf00] use an al- gebraic denotational style for clearer modular proofs, based on state transfor- mations resp. predicate transformers. Mechanical proofs are often based on interpreter semantics, a further variant of the operational style [Stoy77], and sometimes include high level compiler implementation verification (step 2) with e.g. HL = Stanford-Pascal [Polak81] or Boyer/Moore-Lisp [Moore88, Flatau92, Moore96] or Standard-ML [Curzon93a, Curzon94]. M. Broy [Broy92] uses the Larch-prover [Garland/Guttag91]. One should keep in mind, however, that the running theorem prover implementations are, strictly speaking, not completely verified. Their correctnesses again de- pend on existing correct initial host com- pilers, which are not available up to now. Recalling section 1, hackers might have intruded Trojan Horses [Thomp- son84, Goerigk99b] via unverified start up compilers. Hence, we are left on hu- man checkability of mechanical proof protocols (a-posteriori-proof checking). Теоретические и методологические основы программирования 11 High level compiler implementa- tion verification (step 2) is a field within software engineering. Correct implemen- tation rules have been worked out in many formal software engineering meth- ods and projects like VDM [Jones90], RAISE [George+92], CIP [Bauer78, Partsch90], PROSPECTRA [Hoffmann/- Krieg-Brueckner93], Z [Spivey92], B [Ab- rial+91], and also the PVS-system [Dold00]. Literature on low and machine level compiler implementation verifica- tion (step 3) is by far too sparse. There are only demands by some researchers like Ken Thompson [Thompson84], L.M. Chirica and D.F. Martin [Chirica/Mar- tin86] and J S. Moore [Moore88, Mo- ore96], no convincing realistic methods. Here is the most serious logical gap in full compiler verification. Unfortunately, a majority of software users and engi- neers – as opposed to mathematicians and hardware engineers – do not feel logical gaps to be relevant unless they have been confronted with a counter- example. So we need A. convincing realistic methods for low level implementation verification (step 3) B. striking counter-examples (fail- ures) in case only step 3 has been left out. Let us first step into B and hence go on with an initial discurs on the po- tential risk of omitting the low level ma- chine code verification step for compilers: It is possible to construct a mali- cious compiler executable which cor- rectly compiles any but exactly two source programs [Goerigk99b, Thomp- son84]. One exception can be chosen ar- bitrarily, and the compiler can be con- structed to generate arbitrary, perhaps catastrophic target code – for instance a security relevant back door in the Unix login procedure. The second exception is the compiler's own source code. The ex- ecutable will reproduce itself if applied to this source code. If such a compiler gets used by accident as the pre-initial auxil- iary tool for compiler implementation, without checking its result, it will pro- duce an executable which still behaves maliciously, generates incorrect code for two programs, and one of them might eventually cause a catastrophe. It is very unlikely to find this program and thus such a hidden Trojan Horse by classical testing or compiler validation. Even Wirth's bootstrap test is passed, because the incorrect executable is constructed to reproduce itself in that case, and of course arbitrarily often, no matter if the compiler has been verified on source level or not. Additional low-level implementa- tion verification guarantees correctness and the absence of such malicious behav- ior. The initial compiler executable then provides a trusted execution basis neces- sary in particular also for achieving secu- rity. This is the topic of the companion paper [Goerigk/Langmaack01b]. 4. Towards Trusted Realistic Compilation Experience in realistic compiler construction shows that in order to con- struct correct compilers we are allowed to restrict ourselves to sequential imperative programming languages. For compilation we need no process programming nor any reactive or real-time behavior; compilers are sequential (and transformational) and we only depend on the correctness of their resulting target programs. This in- sight crucially facilitates the foundational investigation in full compiler correctness proofs including the essential (and so far missing) implementation correctness proofs for executable compiler host ma- chine code. Implementations of realistic compilers are constructed • in sequential, mostly in impera- tive languages, • even if concurrent process or real-time languages are to be compiled. Consequently, we will study cor- rect realistic compilation for sequential imperative programming languages, and in particular we restrict ourselves to transformational programs (cf. Section 5), because we are mainly interested in the input/output relations defined by pro- gram semantics. We need full compiler correctness proofs only Теоретические и методологические основы программирования 12 • for one initial compiler per processor family with identified target and host machine language TML = HML • and for one sufficiently high- level source language SL which allows for formulating compilers and system pro- grams. All further compilers, e.g. optimiz- ing compilers or those for more expres- sive system programming languages SL1, compiler generators, any further systems software like provers, proof assistants and proof checkers need no further correct implementation steps below SL or SL1. In particular, no further machine code in- spection is necessary, and executable bi- nary versions of these programs can be generated purely mechanically following N. Wirth [Wirth77]. The resulting code is proved to be correct due to a bootstrap- ping theorem [Goerigk/Langmaack01b], also found in [Langmaack97a, Goe- rigk99a, Goerigk/Langmaack01, Goerigk- /Langmaack01a]. As a conclusion we want to stress, that the second software production process gap (cf. [Goerigk/- Langmaack01b]) can be closed if the Verifix-recipes of correct initial compilers and a-posteriori program-checking [Goe- rigk/Langmaack01b] are obeyed. In the context of the Verifix-project we will furthermore demonstrate how to develop correct compiler generating tools and how to incorporate even unverified existing tools in a fully trusted and rigor- ously proved correct manner [Heber- le+98, Gaul+99, Gaul+96]. Moreover, the specification and verification system PVS [Owre+92] is used for mechanical proof support, in particular for the for- malization and verification of the compil- ing specifications, and for providing sup- port for high level compiler implementa- tion verification using a transformational approach. In the following we want to focus on how to develop a proved correct and hence trustworthy initial compiler im- plementation which we believe is the foundational basis for the practical con- struction of safe and secure, i.e. trustwor- thy executable software. 4.1. Three Steps towards Fully Correct Compilers. In his work on Piton's verified translation [Moore88, Moore96] J S. Moore recommends three steps in or- der to present a convincing correctness proof of a compiler written (or imple- mented) in executable binary host ma- chine code HML: 1. Specification of a compiling re- lation C between abstract source and tar- get languages SL and TL, and compiling (specification) verification w.r.t. an ap- propriate semantics relation ⊑ between language semantics [[٠]] SL, [[٠]] TL. 2. Implementation of a correspond- ing compiler program τHL in a high level host language HL close to the specifica- tion language, and high level compiler implementation verification (w.r.t. C and to program representations φSL SL‘ and φTL TL‘). 3. Implementation of a correspond- ing compiler executable τHML written in binary host machine language HML, and low level compiler implementation verifi- cation (with respect to [[ τHL ]] HL and pro- gram representations φSL‘ SL‘‘ and φTL‘ TL‘‘ ). If we work through every step, then τHL resp. τHML is a correct or verified compiler (implementation). If we want to stress that a correctness proof has been achieved even for a compiler executable like τHML on a real processor, then we sometimes call it fully correct (verified) as informally explained before. Figure 2 in- formally outlines the three essential steps that we have to work through for the construction and verification of fully cor- rect compilers, and in particular of fully correct initial compiler executables. We will make everything shown in this dia- gram precise in the following sections 5 and 6, and in particular we refer to sec- tion 6.3.1, which discusses Figure 2 pre- cisely. 5. Transformational Programs We model the semantics of trans- formational programs by partial relations (or multivalued partial functions) f be- tween input domains Di and (not neces- Теоретические и методологические основы программирования 13 Fig 2. Three steps for correct compiler implementation τHML sarily different) output domains Do. Thus, a program semantics is a subset f ⊆ Di × Do which we often will write as f ∈ Di ⇀Do (= 2 Di × Do) or as Di ⇀f Do; sometimes we also use f : Di ⇀ Do. In case f is single- valued, we may also use → instead of ⇀. We use ";" to denote the well-known se- mantical relational composition, i.e. if f1: D1 ⇀ D2 and f2: D3 ⇀D4, then f1 ; f2 =def =def{ (d1,d4) \| ∃ d2 ∈ D2 ∩ D3 s.t. (d1,d2) ∈ f1 and (d2,d4) ∈ f2 } ∈ D1⇀D4. Data or ele- ments are often program or memory states or pairs of program and memory states (sometimes called configurations with control and data flow components) which we simply call states as well. Data in Di and Do are considered regular or non-erroneous. In order to han- dle irregular data, i.e. finite and infinite errors, we assume that every data domain D is extended by an individually associ- ated disjoint non-empty error set Ω, i.e. DΩ =def D ⊎ Ω and D ∩ Ω = ∅. For every transforma- tional program semantics f we assume an extended version f ∈ Di Ω ⇀ Do Ω which we denote by the same symbol f unless this will cause ambiguities. We have Di Ω = Di ⊎ Ωi and Do Ω = Do ⊎ Ωo. Errors are final. No computation will ever recover from an error2. Thus, we require (the extended) f to be error strict, i.e. f to be total on Ωi and f (Ωi) ⊆ Ωo. However, we have to respect a further phenomenon. Errors are of essentially dif- ferent types. They are either unavoidable and we have to accept them, like for in- stance machine resource violations, or they are unacceptable and thus to be avoided. We will allow unacceptable er- rors to cause unpredictable (or chaotic) consequences. In order to model this phenomenon, we partition Ω in a non- empty set A ⊆ Ω of acceptable and a non- empty set U =def Ω \ A of unacceptable or chaotic errors. So we require Ωi = A i ⊎ Ui and Ωo = A o ⊎ Uo and a strong error strictness, namely that f is total on Ωi (and thus on Ai and Ui) and f (A i) ⊆ A o and f (U i) ⊆ Uo . The error sets Ω are supposed to contain a particular standard error ele- ment ⊥ which is to model infinite compu- tation (divergence). So in particular we have ⊥o ∈ Ωo, and for extended program semantics f we additionally require (d, ⊥o) ∈ f or equivalently ⊥o ∈ f(d) when- ever there is a non-terminating (infinite) computation of f starting with d ∈ Di Ω. 2 Note that exceptions are not errors in our sense. We think of exceptions as special cases of non-local regular control flow. Теоретические и методологические основы программирования 14 Thus, we model transformational program semantics by strongly error strict extended relations between extended in- put and output domains, and we addi- tionally require them to meet the above condition for infinite computations. 5.1. Correct Implementation. Let fs be a source and ft a target program se- mantics. In the following we will explain when ft correctly implements fs. This re- quires data representation relations ρi ∈ Di s Ω ⇀ D i t Ω and ρo ∈ Do s Ω ⇀ Do t Ω between source and target input and output data. Both relations, ρi and ρo, and their in- verses ρi -1 and ρo -1, have to be strongly error strict (we sometimes call such ρ's strongly error strict in both directions). Fig 3. Source and target program semantics fs, ft and data representations ρi, ρo Definition 5.1. (Correct implemen- tation or refinement) ft is said to be a cor- rect implementation or refinement of fs relative ρi and ρo and associated error sets, iff ( ρi ; ft ) (d) ⊆ ( fs ; ρo) (d) ∪ Ao t holds for all d ∈ Di s where fs (d) ⊆ Do s ∪ Ao s (which is equivalent to ( fs ; ρo) (d) ⊆ Do t ∪ ∪Ao t , because ρo is strongly error strict in both directions). For any target program computa- tion, the outcome d'' in Do t Ω is either an acceptable error output in Ao t, or there exists a source program computation that either ends in a (regular) d' correspond- ing to d'' or with an unacceptable (cha- otic) error output in Uo s. That is to say: If ft is a correct im- plementation of fs, then ft either returns a correct result, or an acceptable error, or, if fs can compute an unacceptable error, ft may (chaotically) return any result, be- cause we do not require anything in that case. If ft correctly implements fs relative ρi and ρo, we will write ρi ; ft ⊒ fs ; ρo or even shorter just ft ⊒ fs (with a boldface ⊒). We indicate this diagram commuta- tivity by the diagram in Figure 4 and we will later see that we can compose cor- rect implementation diagrams both verti- cally and horizontally, which is a very important fact for practical software en- gineering and compiler generation. Fig 4: Commutative diagram expressing correct implementation There are some variations of cor- rect (relative) implementation as of Defi- nition 1, which we would like to discuss: We speak of correct acceptable imple- mentation resp. of correct regular imple- mentation or refinement, iff ∅ ≠ ( ρi ; ft )(d) ⊆ ( fs; ρo)(d) ∪ Ao t acceptable ∅ ≠ ( ρi ; ft )(d) ⊆ ( fs ; ρo)(d) regular holds for all d ∈ Di s where ∅ ≠ fs (d) ⊆ Do s ∪ ∪Ao s resp. ∅ ≠ fs (d) ⊆ Do s. But note that – in contrast to the different program cor- rectness notions (cf. Section 5.1.1) – all three implementation correctness notions are independent; neither one implies the other. It is remarkable, however, that concrete correctness proofs turn out to be of less complexity if ⊥ is supposed to be unacceptable, i.e. if we prove variants of correct regular implementation [Mueller- Olm/Wolf00, Wolf00]. If ⊥ is supposed acceptable, then our experience shows, that we have to characterize greatest fixed points exactly and to additionally use computational or fixed point induc- tion in order to prove variants of correct acceptable implementation, e.g. preserva- tion of partial correctness [Goerigk00a, Goerigk00b]. 5.1.1. Preservation of Relative Correctness. It is an important observa- Теоретические и методологические основы программирования 15 tion, that we can exactly characterize cor- rect implementation by preservation of relative correctness [Wolf00], which gen- eralizes Floyd's and Hoare's notions of partial respectively total program cor- rectness. Let f ∈ Di Ω ⇀ Do Ω be a program semantics and let Φ ⊆ Di and Ψ ⊆ Do be predicates, i.e. subsets of regular data. Definition 5.2. (Relative program correctness) f is called (relatively) correct with respect to (pre- and post-conditions) Φ and Ψ (<Φ> f <Ψ> for short), iff f (Φ) ⊆ Ψ ∪ Ao . If there is no ambiguity, and if the implicit parameters are clear from the context, we will sometimes leave out the word relative and simply speak of pro- gram correctness. The following theorem says that ft correctly implements fs if and only if relative correctness of fs implies relative correctness of ft for all pre- and post-conditions Φ and Ψ. Theorem 5.1. (Preservation of rela- tive correctness) ft correctly implements fs (ρi ; ft ⊒ fs ; ρo) if and only if, for all Φ ⊆ Di s and Ψ ⊆ Do s, <Φ> fs <Ψ> ⇒ < ρi(Φ) > ft < ρo(Ψ) >. Proof. Only if: Let fs (d) ⊆ Do s ∪ Ao s imply (ρi ; ft ) (d) ⊆ ( fs ; ρo ) (d) ∪ Ao t for all d ∈ Di s and let fs (Φ) ⊆ Ψ ∪ Ao s. Claim: ft (ρi(Φ)) ⊆ ⊆ ρo(Ψ) ∪ Ao t. In order to show this, let d ∈ Φ. Then fs (d) ⊆ Ψ ∪ Ao s ⊆ Do s ∪ Ao s. Hence, ft (ρi (d)) ⊆ ρo( fs (d)) ∪ Ao t ⊆ ρo(Ψ ∪ Ao s) ∪ Aot = ρo(Ψ) ∪ Ao t . If: Let fs(Φ) ⊆ Ψ ∪ Ao s imply ft (ρi (Φ)) ⊆ ρo(Ψ) ∪ Ao t for all Φ ⊆ Di s and Ψ ⊆ Do s, and let fs (d) ⊆ Do s ∪ Ao s. Claim: (ρi ; ft ) (d) ⊆ ( fs ; ρo) (d) ∪ Ao t. For this, let Φ =def {d} and Ψ =def fs (d) ∩ Do s. Then fs(Φ) = fs (d) = ( fs (d) ∩ Do s ) ∪ ( fs (d) ∩ Ao s ) ⊆ ⊆Ψ ∪ Ao s . So (ρi ; ft )(d) ⊆ ρo( fs (d) ∩ Do s ) ∪ Ao t ⊆ ⊆ ( fs ; ρo)(d) ∪ Ao t . Note that this theorem remains valid even if we relax strong error strict- ness; we actually need not require ρi and ρo and their inverses to be total on error sets. We only need that they respect the partition in acceptable and unacceptable errors. However, we still prefer data rep- resentation relations to be total on error sets (in both directions). Again, we may discuss variations of the notion of relative program correct- ness, i.e. acceptable program correctness resp. regular program correctness with respect to pre-conditions Φ ⊆ Di and post- conditions Ψ ⊆ Do: <Φ> f <Ψ>acc iff ∅ ≠ f(d) ⊆ Ψ ∪Ao (acceptable) <Φ> f <Ψ>reg iff ∅ ≠ f (d) ⊆ Ψ (regular) respectively hold for all d ∈ Φ. Note that regular program correctness implies ac- ceptable program correctness, which im- plies relative program correctness. Fur- thermore, correct acceptable resp. regular implementation is equivalent to preserva- tion of acceptable resp. regular program correctness, i.e. ft correctly acceptably resp. regularly implements fs if and only if <Φ> fs <Ψ>acc ⇒ <ρi (Φ)> ft <ρo (Ψ)>acc (acceptable) <Φ> f <Ψ>reg ⇒ <ρi (Φ)> ft <ρo (Ψ)>reg (regular) respectively holds for all Φ ⊆ Di s and Ψ ⊆ Do s. 5.1.2. Classical Notions of Correct Implementation. In which sense does relative or acceptable or regular program correctness generalize the classical no- tions of partial or total program correct- ness? Let f be an original, i.e. unextended program semantics f ∈ Di ⇀Do and let Φ ⊆ Di and Ψ ⊆ Do be pre- and post-conditions, respectively. f is called partially correct w.r.t. Φ and Ψ ({Φ} f {Ψ} for short), if f (Φ) ⊆ Ψ. f is called totally correct w.r.t. Φ and Ψ ([Φ] f [Ψ] for short), if f is partially correct w.r.t. Φ and Ψ, i.e. f (Φ) ⊆ Ψ, and additionally the domain dom f of f comprises Φ, i.e. if additionally dom f ⊇ Φ. Теоретические и методологические основы программирования 16 Let us now choose the same par- ticular error sets A = Ai = Ao =def {a} and U = Ui = Uo =def {u} for both domains Di and Do with ⊥ ∈ {a,u} and Ω = Ωi = Ωo =def =def A⊎U, and extend f to f ext∈ Di Ω⇀Do Ω by f ext =def f ∪ ((Di \ dom f ) × {⊥}) ∪ idΩ f ext is strongly error strict, regardless of ⊥ being considered acceptable (Ai = Ao =def =def {⊥}, Ui = Uo =def {u}) or unacceptable (A i = Ao =def {a}, Ui = Uo =def {⊥}). dom(f ) =def =def dom f is the domain of f. Partial and Total Program Correct- ness. Relative and acceptable correctness are equivalent to partial correctness <Φ> f ext <Ψ> ⇔ <Φ> f ext <Ψ>acc ⇔ {Φ} f {Ψ} if ⊥ = a is considered acceptable, and relative, acceptable and regular correct- ness are equivalent to total correctness, if ⊥ = u is considered unacceptable: <Φ> f ext <Ψ> ⇔ <Φ> f ext <Ψ>acc ⇔ ⇔ <Φ> f ext <Ψ>reg ⇔ [Φ] f [Ψ] Preservation of Partial and Total Program Correctness. It is not only that relative program correctness generalizes classical partial and total program correct- ness. Our notion of correct (relative) im- plementation also generalizes well-known implementation correctness notions. Fig 5: Classical correct implementation versus preservation of relative correctness. Consider a classical unextended implementa- tion diagram (a). If we extend fs and ft as ex- plained before, and if we extend the data representation relations ρi and ρo by ρi ext =def =def ρi ∪ idΩ respectively ρo ext =def ρo ∪ idΩ as well, then we get the extended diagram (b). If we consider ⊥ acceptable, then ρi ext ; ft ext ⊒ fs ext ; ρo ext ⇔ ρi ; ft ⊆ fs ; ρo exactly expresses preservation of partial program correctness. On the other hand, if we consider ⊥ unacceptable, then ρi ext ; ft ext ⊒ fs ext ; ρo ext ⇔ ⇔ (ρi ; ft ) \| dom( fs ; ρo) ⊆ fs ; ρo and dom ρi ; ft ⊇ dom fs ; ρo expresses exactly the classical preserva- tion of total correctness. Hence, it is justified to transfer the terms total and partial to extended func- tions or relations f ext, and we may use the words ``correct total (resp. partial) imple- mentation'' instead of "correct regular (resp. relative) implementation". Also, we may replace "regular (resp. relative) pro- gram correctness" again by "total (resp. partial) program correctness". The classical software engineering notion of correct implementation as propagated in many (also formal) soft- ware engineering approaches like for in- stance in VDM (Vienna Development Method) is preservation of total program correctness. We should, however, keep in mind that resources might well exhaust while machine programs are executed on real target machines, so that a compiled program semantics ft can in general not be proved to meet the requirements of correct implementation in the latter sense. Preservation of relative correctness gives us the necessary means to define adequate notions of correct implementa- tion also for realistic correct compilation. 5.2. Composability. We men- tioned that composability (transitivity) of correct implementation is crucial for modular software construction and verifi- cation, and in particular for stepwise compilation and compiler construction and implementation. In the following we prove vertical and horizontal transitivity, i.e. that we may (vertically) decompose correct implementations into steps (or phases), and that correct implementation distributes (horizontally) over sequential (relational) composition. In both cases we Теоретические и методологические основы программирования 17 will prove a more generally applicable transitivity result as well. Fig 6: Vertical composition expressed by commutative diagrams: If the inner diagrams are commutative, then so is the outer one. Theorem 5.2. (Vertical transitivity of correct implementation) If ft correctly implements fs, and if ft‘ does so for ft , then ft‘ correctly implements fs. Proof. Let Φ ⊆ Di s, Ψ ⊆ Do s and let <Φ> fs <Ψ> . Then, due to Theorem 5.1, we have <ρi(Φ)> ft <ρo(Ψ)> (commutativity of the upper diagram) and <ρi' (ρi(Φ))> ft‘ <ρo' (ρo(Ψ))> (commutativity of the lower diagram for pre-condition ρi (Φ) and post- condition ρo(Ψ)). But the latter just means <(ρi ; ρi') (Φ)> ft‘ <(ρo ; ρo') (Ψ)> which completes the proof due to equiva- lence of correct implementation and preservation of (relative) correctness (Theorem 5.1). Theorem 5.3 (Horizontal transitivity of correct implementation) If ft correctly implements fs, and if ft‘ does so for fs‘, then ft ; ft‘ correctly implements fs ; fs‘. Fig 7: Horizontal composition expressed by commutative diagrams: If the inner diagrams are commutative, then so is the outer one. Proof. Let (1) ρi ; ft ⊒ fs ; ρo and (2) ρo ; ft ⊒ fs ; ρo' and (3) (fs ; fs‘ ) (d) ⊆ Do s‘ ∪ Ao s‘ Claim: (ρi ; ft ; ft‘)(d) ⊆ ( fs ; fs‘; ρo')(d) ∪ ∪ Ao t‘. Note that (f ; g)(d) = g(f (d)) and that '';'' is associative and monotonic in both arguments. By (3) we have fs‘(fs(d)) ⊆ Do s‘ ∪ ∪Ao s‘ and by ((2), commutativity of the right diagram) and associativity of '';'' we get (ρo; ft‘)(fs(d)) ⊆ (fs‘ ; ρo') (fs(d)) ∪ Ao t‘ and hence (4) ft‘((fs ; ρo)(d)) ⊆ (fs ; fs ; ρo')(d) ∪ Ao t‘ and also (5) ft‘((fs ; ρo)(d) ∪ Ao t ) ⊆ ( fs ; fs‘; ρo')(d) ∪ Ao t‘. The latter holds by strong error strictness of ft‘, i.e. ft‘ (Ao t) ⊆ Ao t‘, from (4). By strong error strictness of fs‘ and (3) we have fs(d) ⊆ Do s ∪ Ao s. Thus, by ((1), com- mutativity of the left diagram) we get (6) (ρi ; ft) (d) ⊆ ( fs ; ρo)(d) ∪ Ao t and finally, by monotonicity of relation composition, (6) and (5) we get (7) ft‘((ρi ; ft ) (d)) ⊆ ( fs ; fs‘ ; ρo')(d) ∪ Ao t‘ which is nothing but our claim. An alter- native equivalent calculation would be (ρi ; ft ; ft‘)(d) = ft‘ ((ρi ; ft)(d)) ⊆ ft‘((fs ; ρo)(d) ∪ ∪ Ao t) ⊆ ft‘ ((fs ; ρo)(d)) ∪ Ao t‘= = (ρo ; ft‘)(fs (d)) ∪ Ao t‘ ⊆ (( fs‘ ; ρo')( fs (d)) ∪ ∪ Ao t‘) ∪ Ao t‘ = (fs ; fs‘ ; ρo')(d) ∪ Ao t‘. Unfortunately, we have to prove horizontal transitivity in a different style. A proof as elegant as for vertical com- posability would require program seman- tics, in particular ft‘, to be error strict in both directions, which is of course not the case in general. Note also that both theorems would not hold if we would re- lax the strong error strictness conditions for data representations. In practice we need more generally applicable versions of both the vertical and horizontal transitivity theorem. We will often find intermediate input and output data domains not to be exactly the same. Let, for vertical composition, com- mutative inner diagrams and the outer Теоретические и методологические основы программирования 18 diagram with its data representations ρi ; ρi' and ρo ; ρo' be as in Figure 8. Fig 8. Weak vertical composability: If the inner diagrams are commutative and ft and ft‘‘ appropriately coincide, then the outer diagram is commutative as well. In order to ensure that ρi ; ρi' and ρo ; ρo' are error strict in both directions, we require the intermediate error sets to agree, i.e. Ai t = Ai t‘‘, Ui t = Ui t‘‘, Ao t = Ao t‘‘, and Uo t = Uo t‘‘. Furthermore, let Ii =def ρi(Di s Ω) ∩ ρi' -1( ft -1(Do t‘ Ω)) ⊆ Di t Ω ∩ Di t‘‘Ω Io =def Do t Ω ∩ ρo' –1 (Do t‘ Ω) ⊆ Do t Ω ∩ Do t‘‘ Ω denote appropriate restrictions of domain and codomain (on the intermediate level) of input and output data representations, respectively. Then, if ft contains ft‘‘ on Ii × Io , we can prove the following vertical composition corollary: Corollary 5.1. If the two inner dia- grams of Figure 8 are commutative, if the intermediate error sets agree, and if ft \|Ii × Io ⊇ ft‘‘ \|Ii × Io , then the outer diagram is commutative as well. Proof. Consider the following (coupling) diagram: Since ft \|Ii × Io ⊇ ft‘‘ \|Ii × Io , it is im- mediately clear that this diagram is commutative. Thus, the outer diagram is commutative due to vertical composition Theorem 5.2. For horizontal composition, let commutative (inner) diagrams and the outer diagram with sequential composi- tions fs ; fs‘ respectively ft ; ft‘ be as in Fig- ure 9. Again, for strong error strictness reasons, we require the intermediate error sets to agree, i.e. Ao s = A i s´, Uo s = U i s´, Ao t = Ai t´, and Uo t = U i t´. Fig 9: Weak horizontal composability: If the inner diagrams are commutative and the data representations ρo and ρi' appropriately coincide, then the outer diagram is commutative as well. Let, again, Is =def fs(Di s Ω) ∩ Di s‘ Ω ⊆ Do s Ω ∩ Di s‘ Ω It =def ft (ρi(Di s Ω)) ∩ ft‘ –1(Do t‘ Ω) ⊆ Do t Ω ∩ Di t‘ Ω denote appropriate restrictions of (inter- mediate) domain and codomain of source and target semantics, respec- tively. Then, if the data representation relation ρo is contained in ρi' on Is × It , we can prove the following horizontal com- position corollary: Corollary 5.2. If the two inner dia- grams of Figure 9 are commutative, if the intermediate error sets agree, and if ρo \|Is × It ⊆ ρi' \|Is × It , then the outer diagram is commutative as well. Теоретические и методологические основы программирования 19 Proof. Consider the following (coupling) diagram: Since ρo \|Is × It ⊆ ρi' \|Is × It , it is imme- diately clear that this diagram is commu- tative. Thus, the outer diagram is commu- tative due to horizontal composition Theorem 5.3. Both more general theorems have been proved by construction of commuta- tive coupling diagrams. In both cases, we have been looking for as weak as possible conditions under which we are allowed to compose commutative diagrams. Note, however, that we might sometimes be able to prove commutativity of more complex diagrams from commutativity of constitu- ent diagrams even under weaker assump- tions. Note also, that we might be able to prove correct implementation for a com- posite diagram, even though one or more component diagrams are not commutative. Let us finally note, that every theo- rem and corollary in this section does hold for any of our notions of correct im- plementation, i.e. not only for correct relative (partial) implementation but also for correct acceptable and correct regular (total) implementation. We have defined a family of correct implementation no- tions which allows for more elaborated and sophisticated adjustments to what- ever the practical requirements for cor- rect implementation really are. And the essential (proof engineering) quality of composability and hence modularizeabi- lity is guaranteed for any choice. 6. Correct Compiler Programs Main constituents of a program- ming language are its set L of abstract syntactical programs and its language semantics [[٠]] L : L → Sem L, a partial function from L into an associated seman- tics space Sem L. The domain of [[٠]] L is the set of so-called proper or well-formed programs. In case of a well-formed π and of sequential imperative programming languages we are aiming at, [[π]] L can be defined as a relation between extended input and output data domains Di L Ω and Do L Ω as discussed in the previous sections: [[π]] L ∈ Sem L =def (Di L Ω ⇀ Do L Ω) For a source language SL, a target language TL and proper source programs πs ∈ SL and πt ∈ TL with semantics fs = [[πs]] SL and ft = [[πt]] TL, section 5 defines the semantical relation ft ⊒ fs of correct implementation: Fig 10. Correct implementation for sequential imperative programs Data representations ρi and ρo and associated acceptable and unacceptable error sets are implicit parameters of ⊒. Note also, that ⊒ implicitly defines if we mean preservation of relative (partial), acceptable or regular (total) correctness. We have not yet fixed any one of these parameters. 6.1. Compiling Specifications. Every compiler program establishes a mapping between source and target pro- grams, actually between source and tar- get program representations like for in- stance character sequences on the one and linkable object code format on the other hand. In order to talk about this mapping abstractly and to relate source and target programs semantically, we as- sume that we have or can define a com- piling (or transformation) specification C : SL ⇀ TL, a mathematical relation between abstract source and target programs. C might be given by a closed inductive definition, more or less constructive, or by a set of Теоретические и методологические основы программирования 20 bottom-up rewrite rules to be applied by a term or graph rewrite system (e.g. bot- tom up rewrite systems, BURS [Pele- gri/Graham88]) as for instance used in rule-based code generators. Fig 11. Correctness of the compiling specification C Definition 6.1 (Correct compiling specification) We call C correct, if and only if for any well-formed source pro- gram πs ∈ SL, every associated target program πt ∈ C(πs) is a correct implemen- tation of πs, i.e. if and only if the diagram in Figure 11 is commutative in the sense ([[٠]] SL -1; C) ⊆ (⊑; [[٠]] TL –1). Note that we do not require C to be defined for all well-formed SL- programs, and we will also not require this property for compiler program se- mantics. Due to resource restrictions of finite host machines we won't be able to prove it for compiler programs, anyway, because realistic source languages con- tain arbitrarily large programs. For any two programming lan- guages SL and TL there is an implicitly given natural correct compiling specifica- tion that simply relates any well-formed source program in SL to every of its cor- rect implementations in TL: ℂ =def [[ ٠]] SL ; ⊑ ; [[٠]] TL –1 The following calculation shows, that ℂ is correct (Actually, if we only consider well-formed programs, it is the largest correct compiling specification.): ([[٠]] SL –1 ; ℂ) = = ([[٠]] SL –1 ; [[٠]] SL ; ⊑ ; [[٠]] TL –1) ⊆ (⊑; [[٠]] TL –1). But how is a correct C related to ℂ in general? Of course, ℂ ⊈ C (C might even be empty, e.g. for the pathological compiler which fails on every source pro- gram). Restricted to well-formed source programs, C is a subset of ℂ. However, in general C might relate non well-formed SL-programs (which have no semantics) to TL-programs. Perhaps well-formedness is hard to decide or even undecidable. So compilers sometimes generate or have to generate target code also for improper source programs without explicitly sig- naling an error. The user should be care- ful, keep this in mind and avoid non- well-formed compiler inputs. In any case, in general C ⊈ ℂ as well. Hence, so far C is unrelated to ℂ, and so will be any correct implementa- tion of C. This observation suggests to view at the program sets SL and TL as data domains and extend them by par- ticular unacceptable error elements. This will allow us to also formally express in particular the well-formedness precondi- tion that source programs have to fulfill if they are to be correctly compiled. We will do so also for the semantics spaces SemSL and Sem TL . For SLΩ and TLΩ we need an unac- ceptable error nwf (for "non-well-formed") in USL and UTL, and for SemSL Ω and SemTL Ω we need an unacceptable error uds (for "undefined semantics") in USemSL and USemTL. C, ℂ, [[٠]] SL, [[٠]] TL and ⊑ are extended so that these artificial error ele- ments are related to each other and to non-well-formed programs in SL and TL. Again we denote the extended relations by the same symbols. Observe in Figure 12 (b), that we used ⊒v to indicate the difference be- tween (horizontal) correct implementation ⊒ and (vertical) correct compiler imple- mentation ⊒v (see section 6.3.3). For ⊒v (respectively ⊒v) only preservation of relative (partial) correctness makes sense in practice, i.e. commutativity of diagram (b) is only valid if ⊒v expresses correct relative (partial) implementation. Теоретические и методологические основы программирования 21 Fig 12. Correctness of extended compiling specifications. The original diagrams (a) (for C and ℂ) are commutative if and only if the corresponding extended diagrams (b) are. The extended C is a correct im- plementation of the extended ℂ (Figure 13) and hence this step homogeneously fits on top of a stack of further commuta- tive diagrams establishing correct trans- formation and implementation steps, all correctly tied together and related to ℂ by vertical composability due to Theorem 5.2 and Corollary 5.1 from section 5. As any compiler program, also the compiling specification C reflects design decisions. It already selects particular target pro- grams from the set of all possible correct implementations. Fig 13. Correctness definition for extended compiling specifications Theorem 6.1 (Correct compiling specifications) A compiling specification C is correct, if and only if it is a correct implementation of ℂ. Proof: If: by Figure 13, Figure 12 (b) and vertical composition. Only if: Let πs ∈ SL and ℂ (π s) ⊆ ⊆TL ∪ ATL (), and let πt ∈ C(πs). We have to show: πt ∈ ℂ(πs) ∪ ATL. First note that πs is well-formed, i.e. has semantics [[ πs]] SL ∈ SemSL, because otherwise πt and ℂ(πs) would be the unacceptable error nwf ∉ TL ∪ ATL which contradicts (). If πt ∈ ATL, then we are done. πt ∈ UTL is impossible, because πt would be nwf and hence πs not well-formed. So let πt ∈ TL. Then, ([[ πs]] SL, πt) ∈ ∈ ([[٠] SL –1 ; C). Due to correctness of C (Figure 12 (a)) we have ([[ πs]] SL, πt) ∈ ∈ (⊑; [[٠]] TL –1), that is to say (πs, πt) ∈ ∈ ([[٠]] SL ; ⊑ ; [[٠]] TL —1). But the latter is exactly the definition of ℂ, hence we have πt ∈ ℂ(πs). 6.2. Correct Compiler Programs. In order to prove that a compiler program (sometimes also called compiler implementation or simply compiler) is correct, we want to relate its semantics to the compiling specification. It is often a good advice to write a compiler in its own source language. In general, though, the compiler will be imple- mented in a high level or a low level machine host language HL with seman- tics space SemHL Ω = (Di HL Ω ⇀ Do HL Ω )Ω. If we want to call an HL-program τh a compiler from SL to TL, then we need representation relations φs and φt to rep- resent SL- and TL-programs as data in SL´ Ω =def Di HL Ω resp. in TL´Ω =def Do HL Ω. Note that there are a lot of data in SL´ and TL´ which do not represent pro- grams, but for a consistent presentation we prefer to let a compiler program τh just be like any other HL-program. The situation is as described in Figure 14. However, in order to treat lan- guages of concrete program repre- sentations like SL´ and TL´ as reasonable programming languages, we require that [[٠]] SL´ =def φs –1 ; [[٠]] SL and [[٠]] TL´ =def =def φ t –1 ; [[٠]] TL are single-valued partial functions. Thus, any concrete representa- tion of a well-formed SL- or TL-program has a unique semantics. Теоретические и методологические основы программирования 22 Fig 14. Compiler programs related to compil- ing specifications. If the lower diagram is commutative as well, we call τh a correct compiler program Definition 6.2 (Correct compiler program) We call τh a correct compiler program, iff [[τh]] HL ⊒ ℂ, i.e. iff [[τh]] HL is a correct implementation of ℂ. If τh is a correct compiler, then the lower diagram of Figure 14 and, due to vertical composition, also the outer dia- gram is commutative. Actually, we could equivalently have required ⊒-commuta- tivity of the outer diagram. This would entail commutativity of both inner dia- grams and in particular of the lower dia- gram (the upper diagram is commutative anyway). The proof of the latter remark is a bit more detailed, but analogous to that of Theorem 6.1: Let πs ∈ SL and φt (ℂ(πs)) ⊆ ⊆ TL´ ∪ ATL´ (), and let π't ∈ [[πs]] SL(φs (πs)). We have to show π't ∈ φt(ℂ(πs)) ∪ ATL´. First note that πs is well-formed, i.e. has semantics [[πs]] SL. Otherwise, ℂ would as- sign nwf ∈ UTL to πs which contradicts (). If π't ∈ ATL´ , we are done. If π't ∈ UTL´, then by commutativity of the outer dia- gram [[πs]] SL∈ (⊑; [[٠]] TL´ –1)–1 (UTL´) = {uds} contradicting well-formedness of πs. So let π't ∈ TL´. Commutativity of the outer diagram means ([[٠]] SL´ –1 ; [[τh]] HL)([[πs]] SL) ⊆ ⊆ (⊑; [[٠]] TL´ –1)([[πs]] SL) ∪ ATL´ and therefore π't ∈ (⊑; [[٠]] TL´ –1)([[πs]] SL) = φt([[٠]] TL —1 (⊑ ⊑ ([[πs]] SL))). Since π't and [[πs]] SL are regu- lar in TL´ resp. SemS, we have π't ∈ ∈ φt (ℂ(πs)) by definition of ℂ. Any correct compiler program τh in- duces an associated correct extended com- piling specification Cτ =def (φs ; [[τh]] HL ; φt –1) : SLΩ ⇀ TLΩ such that [[ τh ]] HL ⊒ C τ ⊒ ℂ . If [[τh]] HL is a correct implementa- tion of any correct specification C, i.e., [[ τh ]] HL ⊒ C ⊒ ℂ, then τh is a correct compiler program (cf. Figure 15). That is to say: A compiler program is correct, if and only if it is the correct implementa- tion of a correct compiling specification. Fig 15. Compiler programs and compiling specifications. Due to vertical composition, a correct implementation of a correct compil- ing specification is a correct compiler But what does happen, if we apply a correct compiler program to the represen- tation of a well-formed source program? It should not be a surprise, that we will get at most a representation of a correct im- plementation of the source program: Theorem 6.2. Let τh be a correct compiler program and let π's ∈ φs(πs) be the representation of a well-formed SL-program. Then any regular π't ∈ ∈ [[τh]] HL(π's) represents a correct imple- mentation πt of πs. Proof: Since πs is well-formed, ℂ(πs) ⊆ TL and hence, since τh is a correct compiler program, we have (φs ; [[τh]] H L)(πs) ⊆ ⊆ (ℂ;φt) (πs) ∪ Ao HL. Thus, π't ∈ [[ τh ]] HL (π's) ⊆ [[ τh ]] HL (φs(πs)) ⊆ ⊆ (ℂ;φt) (πs) ∪ Ao HL . Теоретические и методологические основы программирования 23 But π't is regular, i.e. π't ∉ Ao HL. Therefore, π't ∈ (ℂ;φt) (πs). So π't ∈ φt(πt) for a πt ∈ ∈ ℂ(πs), which means [[πt]] TL ⊒ [[πs]] SL. Let us call a concrete SL´- or TL´- datum π's or π't a well-formed SL´- or TL´- program, if it represents a well formed SL- or TL-program. Then π's or π't have semantics [[π's]] SL´ respectively [[π't]] TL´. Thus, it is defined when π't correctly im- plements π's. According to Theorem 6.2, every regular result π't ∈ [[ τh ]] HL (π's) of a correct compiler τh, applied to a well- formed π's, correctly implements π's. That is to say: A correct compiler, applied to a well-formed source program, returns at most correct implementations of that source program. 6.3. Discussion and First Sum- mary. We want to summarize some im- portant observations and give some addi- tional explanations. In particular, we will relate the definitions and notions defined in the previous sections to our informal sketch of a conscientious compiler cor- rectness proof as of section 4.1 and in particular of Figure 2. Moreover, we will discuss McKeeman's T-diagram notation, give some remarks on the difference be- tween correct implementation of user programs and of compiler programs, and finally we want to discuss correct imple- mentation for optimizing compilers. 6.3.1. Precise View at the Three Steps. Let us first come back to the dia- gram shown in Figure 2 (page 13) in sec- tion 4.1. In the previous sections (5, 6.1 and 6.2) we have exactly defined every single notion mentioned in section 4.1 and, hence, we now know precisely every conjecture we have to prove in order to implement an SL to TL compiler correctly as an executable program on a host processor HM. In Figure 2, every data set, pro- gram set and semantics space, every pro- gram semantics, data representation, pro- gram representation, semantics function, compiling specification, compiler seman- tics and semantics relation has to be ap- propriately extended by unacceptable and acceptable error elements. The fol- lowing commutative diagrams (Figure 16 and 17) precisely express that C is a cor- rect compiling specification, and that τHL respectively τHML are correct compiler programs. Programs and their representations have equal semantics. But we should ex- plicitly note that in diagram 16 the com- piler program τHML is not a representa- tion of τHL. These two programs have in general different semantics, but the for- mer is a correct implementation of the latter. Fig 16. This diagram is again illustrating the three steps for correct compiler implementation as of Figure 2 on page ?? Теоретические и методологические основы программирования 24 Fig 17. This diagram is again illustrating correct implementation as of Figure 4 on page ??. Note that [[πSL]] SL = [[π'SL]] SL´ = = [[π''SL]] SL´´ and analogously for TL 6.3.2. T-Diagram Notation. McKee- man's so-called T-diagrams allow to illus- trate the effects of iterated compiler ap- plications in an intuitive way. We use them as shorthand notations for particu- lar diagrams as of Figure 18. Fig 18. The situation which we will abbrevi- ate by McKeeman's T-diagrams Recall that ℂ is the natural correct compiling specification from SL to TL. Well-formed programs and their (syntac- tical) φ-representations have equal se- mantics, and τHL´ ∈ φHL HL´(τHL) is a well- formed HL´-program compiling syntacti- cal SL´-programs to syntactical TL´- programs. HL´ is the domain of perhaps more concrete syntactical representations of HL-programs. In this situation we use T-diagram (Figure 19) as an abbreviation for the diagram in Figure 18. However, we have to keep in mind that the con- crete situation is a bit more involved, Fig 19. McKeeman's T-diagram as a short-hand for the above situation that the T-diagrams do not explicitly ex- press crucial differences between various program representations. We need to dis- tinguish programs, program semantics and (syntactical) program representations in order to suffice requirements from practice. We cannot put practitioners short by elegant but too nebulous ideali- zations. 6.3.3. Correct Implementation ver- sus Correct Compiler Implementation. If we bootstrap compiler programs, we have in general to distinguish between two dif- ferent notions of correct implementation. Source programs are to be correctly im- plemented by target programs (relating source to target programs) on the one hand, and the compiler itself is to be cor- rectly implemented on the host machine (which relates the compiler source pro- gram to the compiler machine program). Error behavior and required parameterization of application programs πSL, πTL and their representations πSL´, πTL´ , πSL´´ , πTL´´ are in general of a different nature and independent of the expected error behavior and required parameteriza- tion for the compiler, i.e. for the specifi- cation C and compiler programs τHL, τHML and their syntactical representations. For instance, let us assume SL to be a process programming language. The process programmer would not like to witness any uncertainty nor error at com- putation time of source programs πSL re- spectively πSL´, πSL´´. That is source pro- grams are written such that ∅ ≠ [[πSL]] SL (di s) ⊆ Dos (1) holds whenever πSL is applied to an input di s ∈ Di s \ [[πSL]] SL -1 (Uo s) outside the domain of computations which possibly end in unacceptable errors. But this involves regular termination and hence total cor- rectness of πSL which the process pro- grammer requires to be preserved for any correct implementation πTL. He/she wants that ∅ ≠ [[ πTL]] TL (di t) ⊆ Dot (2) Теоретические и методологические основы программирования 25 holds whenever the target program πTL is applied upon the representation di t ∈ ρi(di s ), di s ∉ [[πSL]] SL -1(Uo s), of the corresponding input. Correct regular (total) implementa- tion together with (1) guarantees (2), be- cause due to section 5.1, we have ∅ ≠ [[ πTL]] TL(di t) ⊆ ρo( [[ πSL]] SL(di s)) ⊆ Dot. On the other hand, the same proc- ess programmer will (and in general has to) accept compile time error reports, like for instance HM-memory overflow, while πSL is compiled to πTL, i.e. while the com- piler machine implementation τHML is executed and applied upon a (syntactical) representation πSL´´ of the source program πSL. With respect to compilation, the process programmer wants a guarantee at execution time of πTL´´ whenever τHML has succeeded on HM and has generated the target program representation πTL´´, which means that (2) is established by success- ful execution of the compiler implemen- tation τHML. Note that there are no obvious natural mappings between the error sets Ao s, Uo s , Ao t, Uo t crucial for the correct im- plementation of source programs by tar- get programs on the one hand, and the error sets ATL´ =def Ao HL, UTL´ =def Uo HL, ATL´´ =def Ao HML and UTL´ =def Uo HML crucial for the correct implementation notion for generating the compiler machine execu- table τHML on the other hand. We have to distinguish these two correct implementa- tion relations. 6.3.4. Notes on Optimizing Com- pilers. As already mentioned, many exist- ing and in particular optimizing compiler programs τh do not check all pre condi- tions necessary for correct compilation of source programs. In particular optimizing transformations often need pre-conditions which, for practical reasons, are too hard to decide or are even algorithmically un- decidable 3. Therefore, in general compil- 3 For many programming languages it is algo- rithmically undecidable whether or not for in- stance variables are initialized before they are used, or if programs terminate regularly. ing specifications C or compiler program semantics [[ τh ]] HL might yield unreason- able target programs even for well- formed programs for which additional op- timization pre-conditions do not hold. Our more elaborated view at cor- rect implementation offers a remedy which exploits the notion of acceptable errors in ATL. Let us think of a compiler warning (like for instance "Warning: ar- ray index check omitted in line ...") as a potential error message, i.e. as an indica- tion for an eventually generated target program πt to potentially belong to the set of acceptable errors in ATL in the fol- lowing sense: ''We [the compiler] give you [the compiler user] the following tar- get program πt, but it contains optimiza- tions which require additional pre condi- tions Φ ⊆ Di s for your source program to hold. If you cannot guarantee Φ, please take this as an error message, because πt might not be correct.'' That is to say: Besides the usual compiling specification C every source program πs carries an additional (optimi- zation) pre-condition Φ = PC(πs) ⊆ Di s, PC : SL → 2Dis, which leads to a modified source language semantics [[ πs]] SL,PC =def [[ πs]] SL ∪ (Dis\PC(πs)) × {pcf}, where pcf ∈ Uo s reads as "(optimization) pre-condition false". Now, if compiling specification or compiler program deliver a target program together with an opti- mization warning, then this guarantees a weaker correct implementation of πs by πt, namely that (ρi ; [[ πt]] TL) (di s ) ⊆ ([[ πs]] SL; ρo) (di s) ∪ Aot holds for all di s ∈ PC(πs) with [[ πs]] SL(di s ) ⊆ ⊆ Di s ∪ Ao s. This weaker notion of correct implementation (with respect to [[٠]] SL) can equivalently be expressed by usual correct implementation, but with respect to the weaker semantics relation [[٠] SL,PC . A well-known optimization is the so-called redundant (dead) code elimina- tion, which might violate preservation of relative (partial) correctness, e.g. which might eliminate the code that for some Теоретические и методологические основы программирования 26 input data di s ∈ Di s would cause a runtime error like for instance a division by zero. The source program πs might be partially (relatively) correct w.r.t. some pre- and post-conditions Φ´ resp. Ψ´, whereas the optimized target program πt is not. It might return a regular but incorrect re- sult if applied to di t ∉ ρi (Φ). If the addi- tional optimization pre condition Φ does not hold for the input, πt might danger- ously deceive the user. Its result might have nothing in common with any regu- lar source program result do s . A different optimization is the so- called unswitching, which might violate preservation of total (regular) correctness. Unswitching is an optimization that moves conditional branches outside loops and in particular changes the sequential order of conditional expressions while transforming while(b, if (c, π1,π2)) ↦ if (c, while (b, π1), while (b, π2)) . This transformation does in general not preserve regular (total) correctness. A process programmer, who has proved regular (total) correctness of a source program πs (containing the left statement) would dangerously be cheated by the program πt (containing an implementation of the right statement instead) if πt is ap- plied to input data di t ∉ ρi (Φ) such that b evaluates to false and c causes a runtime error. In that case, πt would incorrectly irregularly abort with an error, which might lead to a dangerous situation if πt controls for instance a safety critical process. 7. From Correct Compiler Programs to Trusted Compiler Implementations At this point we have developed a mathematical theory of expressing com- piling and compiler implementation cor- rectness in a compositional, rigorous and realistic way using special commutative diagrams. In particular Figure 16 on page 23 precisely defines the three essential proof obligations corresponding to the three tasks necessary in order to provide a rigorous and conscientious correctness proof for an initial trusted compiler ex- ecutable. It is the machine (low) level com- piler implementation correctness proof by bootstrapping and a-posteriori code in- spection, which is new and for the first time closes the implementation gap rig- orously and trustworthily. It needs further explanation. Therefore, the forthcoming second part of our article on Trusted Compiler Implementation [Goerigk/Lang- maack01b] will go into detail on this proof for the initial trusted compiler ex- ecutable which we have constructed and completely verified. The article will also give a security related motivation for low level implementation verification and show that otherwise correctness and thus trustworthiness cannot be guaranteed. For machine level compiler imple- mentation verification we will use a spe- cialized bootstrapping technique with a- posteriori code-inspection. Initially, a Common Lisp system runs on and gener- ates code for our compiler on an auxil- iary processor. We use it as an unverified compiler generator which transforms its specification (the compiler source pro- gram) and generates an (auxiliary) com- piler machine executable. The generated executable depends on untrusted auxil- iary software and is not verified. Its re- sults have to be checked. Fortunately, we need to use this auxiliary executable only once. N. Wirth's technique of writing the compiler in its own source language en- ables to bootstrap the compiler source again, and this run, if successful, gener- ates a target program which should be the specified target code for the com- piler. Although in general every result of the auxiliary executable would have to be checked, we need a-posteriori result checking only for exactly one run. This is because we realize an im- portant difference to the general proce- dure: As soon as the syntactical check succeeds and guarantees, that the gener- ated binary is as specified by the seman- tically correct compiling specification, a semantics to syntax reduction theorem applies and guarantees that the gener- Теоретические и методологические основы программирования 27 ated binary is a (semantically) correct compiler executable on the target ma- chine. Compiling specification verifica- tion guarantees, that specification com- pliance implies semantical correctness. Source and intermediate languages for the initial compiler are carefully cho- sen in order to be able to finally produce a convincing complete rigorous proof document. They have particularly been chosen to isolate crucial compilation steps and to enable code inspection by target to source code comparison. The compiler will horizontally be decomposed in a (sequential) composi- tion of subsequent passes. Vertical com- position originates from horizontal com- position: The compiler generates a tower of subsequent intermediate programs of decreasing abstraction level between high-level source and machine level tar- get program. Each step (pass) corre- sponds semantically to a commutative diagram expressing that the lower-level intermediate program correctly imple- ments the higher-level program. For the initial compiler every in- termediate program representation is made explicit. Every intermediate lan- guage has an explicit composition opera- tor expressing the (horizontal) sequential composition of passes. If the compiler is applied to itself, then every compiler pass explicitly transforms step by step the se- quential composition of n (= 4) passes to again a sequential composition of n passes. The process finally corresponds semantically to an n by n matrix of com- mutative diagrams (actually n+1 by n in- cluding the specification on top), plugged together by horizontal and verti- cal composition theorems. Semantical machine code inspec- tion – to semantically understand and to assure the correctness of generated target code – is tedious, cumbersome, error- prone and probably unmanageable. But also syntactical machine level code in- spection, i.e. to compare source and ex- pected low-level machine code with re- spect to the (correct) compiling specifica- tion, is cumbersome and should and can be further minimized. Horizontal and ver- tical composition with only two small low level transformations will split the code inspection task in a number of small and easier parts. Lowest level machine code inspection is only necessary for the final code generation. Moreover, the boot- strapping process can already make use of checked lower level passes to guaran- tee implementation correctness for higher level intermediate code, which further helps saving much and in particular low level machine code inspection below the diagonal of the matrix mentioned above. The initial ComLisp compiler uses five subsequent passes including front end and code generation. They are by no means arbitrary. Front end, transforma- tion of recursive procedures using stack technique, of recursive data types imple- mented on a heap memory, of control structure to linear machine code, and code generation producing binary execu- table code, all these passes coincide with passes identifiable also in compilers in general. They also adequately modularize the theorem prover supported mechanical proof of compiling correctness. Acknowledgments We would like to thank our colleagues in the Verifix project for many fruitful discussions, in particular Axel Dold, Thilo Gaul, Gerhard Goos, Andreas Heberle, Friedrich von Henke, Ulrich Hoffmann, Vincent Via- lard, Wolf Zimmermann. Special thanks to Markus Müller-Olm and Andreas Wolf for their contributions to the notion of relative program correctness and its pre- servation. [Abrial+91] J.R. Abrial, M.K.O. Lee, D.S. Neilson, P.N. Scharbach, and I.H. Sørensen. The B-method. In VDM'91: Formal Software Development Methods Volume 2, volume 552 of LNCS, pages 398—405. Springer-Verlag, 1991. [Bauer78] F.L. Bauer. Program development by stepwise transformations – the project CIP. In F. L. Bauer and M. Broy, editors, Program Construction, volume 69 of Lecture Notes in Computer Science, pages 237—266. Springer Verlag, 1978. [Blum+89] M. Blum, M. Luby, and R. Rubinfeld. Program result checking against adaptive pro- grams and in cryptographic settings. In DIMACS Workshop on Distributed Computing and Cryp- thography, 1989. Теоретические и методологические основы программирования 28 [Boerger/Rosenzweig92] E. Börger and D. Rosen- zweig. The WAM-definition and Compiler Cor- rectness. Technical Report TR-14/92, Dip. di In- formatica, Univ. Pisa, Italy, 1992. [Broy92] M. Broy. Experiences with software specification and verification using LP, the larch proof assistant. Technical Report 93, Digital Sys- tems Research Center, Palo Alto, July 1992. [Boerger/Schulte98] E. Börger and W. Schulte. Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation. In 23rd Inter- national Symposium on Mathematical Foundations of Computer Science, LNCS. Springer, 1998. [BSI94] BSI – Bundesamt für Sicherheit in der Informationstechnik.BSI-Zertifizierung. BSI 7119, Bonn, 1994. [BSI96] BSI – Bundesamt für Sicherheit in der Informationstechnik}. OCOCAT-S Projektauss- chreibung, 1996. [Chirica/Martin86] L. M. Chirica and D. F. Mar- tin. Toward Compiler Implementation Correctness Proofs. ACM Transactions on Programming Lan- guages and Systems, 8(2):185—214, April 1986. [Curzon93a] P. Curzon. Deriving Correctness Properties of Compiled Code. Formal Methods in System Design, 3:83-115, August 1993. [Curzon94] P. Curzon. The Verified Compilation of Vista Programs. Internal Report, Computer Labora- tory, University of Cambridge, January 1994. [Dijkstra76] Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. [Dold00] Axel Dold. Formal Software Development using Generic Development Steps. Logos-Verlag, Berlin, 2000. Dissertation, Universität Ulm. [Fagan86] M. E. Fagan. Advances in software in- spections. IEEE Transactions on Software Engi- neering, SE-12(7):744-751, 1986. [Flatau92] A. D. Flatau. A verified implementation of an applicative language with dynamic storage allocation. PhD thesis, University of Texas at Aus- tin, 1992. [Garland/Guttag91] S.J. Garland and J.V. Guttag. A guide to lp, the larch prover. Technical Report SRC Report 82, Digital Systems Research 'Center, 1991. [Gaul+96] Th. Gaul, G. Goos, A. Heberle, W. Zimmermann, and W. Goerigk. An Architec- ture for Verified Compiler Construction. In Joint Modular Languages Conference JMLC'97, Linz, Austria, March 1997. [George+92] C. George, P. Haff, K. Havelund, A. E. Haxthausen, R. Milne, C. B. Nielson, S. Prehn, and K. R. Wagner. The Raise Specifica- tion Language. Prentice Hall, New York, 1992. [Goerigk/Langmaack01] W. Goerigk and H. Langmaack. Compiler Implementation Verifi- cation and Trojan Horses. In D. Bainov, editor, Proc. 9th International Colloquium on Numerical Analysis and Computer Science with Applications, Plovdiv, Bulgaria, 2001. [Goerigk/Langmaack01a] W. Goerigk and H. Langmaack. Compiler Implementation Verifica- tion and Trojan Horses (Extended Draft Version). Technical report, Institut für Informatik, CAU, 2001. Available under http://www.informatik.uni- kiel.de/~wg/Berichte/Plovdiv.ps. [Goerigk/Langmaack01b] W. Goerigk and H. Langmaack. Will Informatics be able to Justify the Construction of Large Computer Based Sys- tems? Part II: Trusted Compiler Implementation. International Journal on Problems in Program- ming, 2002. Forthcoming. [Goerke96] W. Goerke. Über Fehlerbewußtseins- kultur. Mündlicher Diskussionsbeitrag, Informatik- Kolloquium, IBM, Böblingen, 1996. Unpublished, 1996. [Goerigk99a] W. Goerigk. On Trojan Horses in Compiler Implementations. In F. Saglietti and W. Goerigk, editors, Proc. des Workshops Sicher- heit und Zuverlдssigkeit softwarebasierter Systeme, ISTec Report ISTec-A-367, ISBN 3-00-004872-3, Garching, August 1999. [Goerigk99b] W. Goerigk. Compiler Verification Revisited. In M. Kaufmann, P. Manolios, and J S. Moore, editors, Computer Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, 2000. [Goerigk00a] W. Goerigk. Trusted Program Exe- cution. Habilitation thesis. Techn. Faculty, Chris- tian-Albrechts-Universität zu Kiel, May 2000. To be published. [Goerigk00b] W. Goerigk. Proving Preservation of Partial Correctness with ACL2: A Mechanical Compiler Source Level Correctness Proof. In M. Kaufmann and J S. Moore, editors, Proceeding of the ACL2'2000 Workshop, University of Texas, Austin, Texas, U.S.A., October 2000. [Gurevich91] Y. Gurevich. Evolving Algebras; A Tutorial Introduction. Bulletin EATCS, 43:264- 284, 1991. [Gurevich95] Y. Gurevich. Evolving Algebras: Lipari Guide. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995. Теоретические и методологические основы программирования 29 [Gaul+99] Th. Gaul, W. Zimmermann, and W. Goerigk. Construction of Verified Software Sys- tems with Program-Checking: An Application To Compiler Back-Ends. In A. Pnueli and P. Traverso, editors, Proc. FLoC'99 International Workshop on Runtime Result Verification, Trento, Italy, 1999. [Heberle+98]A. Heberle, Th. Gaul, W. Goerigk, G. Goos, and W. Zimmermann. Construction of Verified Compiler Front-Ends with Program-Che- cking. In Proceedings of {PSI} '99: Andrei Ershov Third International Conference on Perspectives Of System Informatics, volume 1755 of Lecture Notes in Computer Science, Novosibirsk, Russia, 1999. Springer Verlag. [Hoare+93] C. A. R. Hoare, He Jifeng, and A. Sampaio. Normal Form Approach to Compiler Design. Acta Informatica, 30:701-739, 1993. [Hoffmann/Krieg-Brueckner93] B. Hoffmann and B. Krieg-Brückner. Program Development by Speci- fication and Transformation. Springer, Berlin, 1993. [HSE01] C. Jones, R.E. Bloomfield, P.K.D. Fro- ome, and {P.G.} Bishop. Methods for assessing the safety integrity of safety-related software of uncertain pedigree (SOUP). Contract Research Report 337/2001, Health and Safety Executive, Adelard, London, UK, 2001. [Jones90] C. B. Jones. Systematic Software Devel- opment Using VDM, 2nd ed. Prentice Hall, New York, London, 1990. [Kaufmann/Moore94] M. Kaufmann and J S. Mo- ore. Design Goals of ACL2. Technical Report 101, Computational Logic, Inc., August 1994. [Langmaack73] H. Langmaack. On Correct Pro- cedure Parameter Transmission in Higher Programming Languages. Acta Informatica, 2(2):110-142, 1973. [Langmaack97a] H. Langmaack. Softwareenginee- ring zur Zertifizierung von Systemen: Spezifika- tions-, Implementierungs-, Übersetzerkorrektheit. Informationstechnik und Technische Informatik it+ti, 39(3):41—47, 1997. [Laprie94] J. C. Laprie, editor. Dependability: ba- sic concepts and terminology. Springer Verlag for IFIP WG 10.4, 1994. [Loeckx/Sieber87] Jacques Loeckx and Kurt Sieber. The Foundations of Program Verification (Second edition). John Wiley and Sons, New York, N.Y., 1987. [Mueller-Olm96] M. Müller-Olm. Modular Com- piler Verification: A Refinement-Algebraic Ap- proach Advocating Stepwise Abstraction, volume 1283 of Lecture Notes in Computer Science. Sprin- ger-Verlag, Berlin, Heidelberg, New York, 1997. [Moore88] J S. Moore. Piton: A verified assembly level language. Techn. Report 22, Comp. Logic Inc, Austin, Texas, 1988. [Moore96] J S. Moore. Piton: A Mechanically Veri- fied Assembly-Level Language. Kluwer Academic Press, Dordrecht, The Netherlands, 1996. [Mueller-Olm/Wolf00] M. Müller-Olm and A. Wolf. On the Translation of Procedures to Fi- nite Machines. In G. Smolka, editor, Programming Languages and Systems. Proceedings of ESOP 2000, volume 1782 of LNCS, pages 290—304, Ber- lin, March 2000. [McCarthy/Painter67] J. McCarthy and J. A. Pain- ter. Correctness of a compiler for arithmetical ex- pressions. In J.T. Schwartz, editor, Proceedings of a Symposium in Applied Mathematics, 19, Mathe- matical Aspects of Computer Science. American Mathematical Society, 1967. [Milne/Strachey76] R. Milne and Ch. Strachey. A Theory of Programming Language Semantics. Chapman and Hall, 1976. [Nielson/Nielson92] H. R. Nielson and F. Nielson. Semantics with Applications: A Formal Introduction. John Wiley & Sons, Chichester, 1992. [Owre+92] S. Owre, J. M. Rushby, and N. Shan- kar. PVS: A Prototype Verification System. In Deepak Kapur, editor, Proceedings 11th Interna- tional Conference on Automated Deduction CADE, volume 607 of Lecture Notes in Artificial Intelli- gence, pages 748—752, Saratoga, NY, October 1992. Springer-Verlag. [Partsch90] H. Partsch. Specification and Trans- formation of Programs. Texts and Monographs in Computer Science. Springer-Verlag, 1990. [Pelegri/Graham88] Eduardo Pelegri-Llopart and Susan L. Graham. Optimal code generation for expression trees: An application of {BURS} the- ory. In ACM-SIGPLAN ACM-SIGACT, editor, Conference Record of the 15th Annual ACM Sym- posium on Principels of Programming Languages (POPL '88), pages 294—308, San Diego, CA, USA, January 1988. ACM Press. [Plotkin81] G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981. [Pofahl95] E. Pofahl. Methods Used for Inspecting Safety Relevant Software. In W. J. Cullyer, W. A. Halang and B. J. Krämer (eds.): High Integrity Programmable Electronic Systems, Dagstuhl-Sem.- Rep. 107, p 13,1995. [Polak81] W. Polak. Compiler specification and verification. In J. Hartmanis G. Goos, editor, Lec- Теоретические и методологические основы программирования 30 ture Notes in Computer Science, number 124 in LNCS. Springer-Verlag, 1981. [Sampaio93] A. Sampaio. An Algebraic Approach to Compiler Design. PhD thesis, Oxford University Computing Laboratory, Programming Research Group, October 1993. Technical Monograph PRG- 110, Oxford University. [Scott70] D. S. Scott. Outline of a Mathematical Theory of Computation. In Proceedings of the 4th Annual Princeton Conference on Information Sci- ences and Systems, pages 169—176, Princeton, 1970. [Spivey92] J. M. Spivey. The Z Notation. Prentice- Hall International Series in Computer Science. Prentice Hall, 1992. [Scott/Strachey71] D. Scott and Ch. Strachey. Toward a mathematical semantics for computer languages, pages 19—46. April 1971. [Stoy77] J.E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Lan- guage Theory. MIT Press, Cambridge, MA., Lon- don, 1977. [Schweizer/Voss96] G. Schweizer and M. Voss. Systems engineering and infrastructures for open computer based systems. Lecture Notes in Com- puter Science, 1030:317—??, 1996. [Thompson84] K. Thompson. Reflections on Trusting Trust. Communications of the ACM, 27(8):761—763, 1984. Also in ACM Turing Award Lectures: The First Twenty Years 1965—1985, ACM Press, 1987, and in Computers Under Attack: In- truders, Worms, and Viruses, ACM Press, 1990. [Wirth77} N. Wirth. Compilerbau, eine Einführung. B.G. Teubner, Stuttgart, 1977. [Wolf00] A. Wolf. Weakest Relative Precondition Semantics - Balancing Approved Theory and Real- istic Translation Verification. PhD thesis, Techni- sche Fakultät der Christian-Albrechts-Universität, Report No. 2013, Kiel, February 2001. [ZSI89] ZSI – Zentralstelle für Sicherheit in der Informationstechnik.IT-Sicherheitskriterien. Bun- desanzeiger Verlagsgesellschaft, Köln, 1989. [ZSI90] ZSI – Zentralstelle für Sicherheit in der Informationstechnik. IT-Evaluationshandbuch. Bundesanzeiger Verlagsgesellschaft, Köln, 1990. Date received: 9.11.2002 About authors Prof. Dr. Wolfgang Goerigk Professor of Institute of Informatics and Applied Mathematics Prof. Dr. Hans Langmaack Professor of Institute of Informatics and Applied Mathematics Місце роботи авторів Institut für Informatik und Praktische Mathematik Christian-Albrechts-Universität zu Kiel, Kiel, Germany Email: wg@informatik.uni-kiel.de, hl@informatik.uni-kiel.de

REALISTIC CORRECT SYSTEMS IMPLEMENTATION

Репозитарії

Схожі ресурси