Building “Correct” CompilersOutlineSlide 3The Seven Grand ChallengesSlide 5Dependable Systems EvolutionWhy the sudden interest?A small but significant stepSlide 9Why are correct compilers hard to build?TestingVerify each compilationProving the whole compiler correctSlide 14gcc-bugs mailing listNeed for AutomationThis seems really hard!Slide 18Brief detour thru ATPSlide 20Focus on OptimizationsCommon OptimizationsConstant Propagation ExamplesConstant Propagation ConditionThe Analysis AlgorithmBuilding the CFGSlide 27Symbolic EvaluationSlide 29Slide 30The Dataflow analysis algorithmExample EvaluationTermination ConditionOther OptimizationsSlide 35Making the problem easierSlide 37Slide 38Slide 39Slide 40The DesignSlide 42The CompilerResultsCobalt  Rhodium  ?CaveatsSlide 47Constant Prop (straight-line code)Adding arbitrary control flowConstant prop inSlide 51Slide 52Proving correctness automaticallyConstant prop revisitedGeneralize to any forward optimizationSlide 56Profitability heuristicsThe two pieces of an optimizationProfitability heuristic example: PRESlide 60Slide 61Slide 62Slide 63The Cobalt LanguageSlide 65Constant prop revisited (again)mayDef in CobaltSlide 68Slide 69Slide 70Slide 71mayPntTo in CobaltSlide 73Expressiveness of CobaltFuture workSummary and ConclusionBuilding “Correct” CompilersBuilding “Correct” CompilersK. Vikram and S. M. Nazrul A.K. Vikram and S. M. Nazrul A.OutlineOutlineIntroduction: Setting the high level contextIntroduction: Setting the high level contextMotivationMotivationDetoursDetoursAutomated Theorem ProvingAutomated Theorem ProvingCompiler Optimizations thru Dataflow AnalysisCompiler Optimizations thru Dataflow AnalysisOverview of the Cobalt SystemOverview of the Cobalt SystemForward optimizations in cobaltForward optimizations in cobaltProving Cobalt Optimizations CorrectProving Cobalt Optimizations CorrectProfitability HeuristicsProfitability HeuristicsPure AnalysesPure AnalysesConcluding RemarksConcluding RemarksOutlineOutlineIntroduction: Setting the high level contextIntroduction: Setting the high level contextMotivationMotivationDetoursDetoursAutomated Theorem ProvingAutomated Theorem ProvingCompiler Optimizations thru Dataflow AnalysisCompiler Optimizations thru Dataflow AnalysisOverview of the Cobalt SystemOverview of the Cobalt SystemForward optimizations in cobaltForward optimizations in cobaltProving Cobalt Optimizations CorrectProving Cobalt Optimizations CorrectProfitability HeuristicsProfitability HeuristicsPure AnalysesPure AnalysesConcluding RemarksConcluding RemarksThe Seven Grand ChallengesThe Seven Grand ChallengesIn Vivo In Vivo  In Silico In SilicoScience for Global Ubiquitous ComputingScience for Global Ubiquitous ComputingMemories for LifeMemories for LifeScalable Ubiquitous Computing SystemsScalable Ubiquitous Computing SystemsThe Architecture of the Brain and MindThe Architecture of the Brain and MindDependable Systems EvolutionDependable Systems EvolutionJourneys in Non-classical computationsJourneys in Non-classical computationsIntroductionThe Seven Grand ChallengesThe Seven Grand ChallengesIn Vivo In Vivo  In Silico In SilicoScience for Global Ubiquitous ComputingScience for Global Ubiquitous ComputingMemories for LifeMemories for LifeScalable Ubiquitous Computing SystemsScalable Ubiquitous Computing SystemsThe Architecture of the Brain and MindThe Architecture of the Brain and MindDependable Systems EvolutionDependable Systems EvolutionJourneys in Non-classical computationsJourneys in Non-classical computationsIntroductionDependable Systems EvolutionDependable Systems EvolutionA long standing problemA long standing problemLoss of financial resources, human livesLoss of financial resources, human livesCompare with other engineering fields!Compare with other engineering fields!Non-functional requirementsNon-functional requirementsSafety, Reliability, Availability, Security, etc.Safety, Reliability, Availability, Security, etc.IntroductionWhy the sudden interest?Why the sudden interest?Was difficult so far, but now …Was difficult so far, but now …Greater Technology PushGreater Technology PushModel checkers, theorem provers, Model checkers, theorem provers, programming theories and other formal programming theories and other formal methodsmethodsGreater Market PullGreater Market PullIncreased dependence on computingIncreased dependence on computingIntroductionA small but significant stepA small but significant stepBuilding Correct CompilersBuilding Correct CompilersIntroductionOutlineOutlineIntroduction: Setting the high level contextIntroduction: Setting the high level contextMotivationMotivationDetoursDetoursAutomated Theorem ProvingAutomated Theorem ProvingCompiler Optimizations thru Dataflow AnalysisCompiler Optimizations thru Dataflow AnalysisOverview of the Cobalt SystemOverview of the Cobalt SystemForward optimizations in cobaltForward optimizations in cobaltProving Cobalt Optimizations CorrectProving Cobalt Optimizations CorrectProfitability HeuristicsProfitability HeuristicsPure AnalysesPure AnalysesConcluding RemarksConcluding RemarksWhy are correct compilers hard to Why are correct compilers hard to build?build?Bugs don’t manifest themselves easilyBugs don’t manifest themselves easilyWhere is the bug – program or compiler?Where is the bug – program or compiler?Possible solutionsPossible solutionsCheck semantic equivalence of the two programs Check semantic equivalence of the two programs (translation validation, etc.)(translation validation, etc.)Prove compilers sound (Prove compilers sound (manuallymanually))Drawbacks?Drawbacks?Conservative, Difficult, Actual code not verifiedConservative, Difficult, Actual code not verifiedMotivationcompilerSourceCompiledProgrun!inputexp-ectedoutputTestingTesting•No correctness guarantees:•neither for the compiled prog•nor for the compilerDIFF•To get benefits, must:•run over many inputs•compile many test casesoutputMotivationVerify each compilationVerify each compilationcompilerSourceCompiledProgSemanticDIFF•Translation validation [Pnueli et al 98, Necula 00] •Credible compilation[Rinard 99] •Compiler can still have bugs.•Compile time increases.•“Semantic Diff” is hard.MotivationProving the whole compiler