DOC PREVIEW
CORNELL CS 612 - Automatic Detection and Repair of Errors in Data Structures

This preview shows page 1-2-3-20-21-22-41-42-43 out of 43 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 43 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

IntroductionExampleSpecification Language, Check & RepairExperienceAutomatic Detection and Repair of Errors in DataStructuresBrian Demski, Martin RinardApril 28, 2005Brian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperience1IntroductionScopeApproach2ExampleModel ConstructionConsistency Constraints3Specification Language, Check & RepairStructure Definition LanguageModel Definition LanguageConstraintsError Detection and Repair4ExperienceBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceScopeApproachMotivationThe problemPrograms manipulate data structuresSoftware error or anomaly causes inconsistencyAssumptions under which software was developed no longerholdsoftware behaves in unpredictable mannerThe solution proposedDo not increase the reliability of the codeSpecify key data structure consistency constraintsDynamically detect and repair data structures violating theconstraintsBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceScopeApproachMotivationThe problemPrograms manipulate data structuresSoftware error or anomaly causes inconsistencyAssumptions under which software was developed no longerholdsoftware behaves in unpredictable mannerThe solution proposedDo not increase the reliability of the codeSpecify key data structure consistency constraintsDynamically detect and repair data structures violating theconstraintsBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceScopeApproachGoalDo not necessarily restore the data structure to previousconsistent state the program was intoDeliver repaired data structures satisfying the consistencyassumptions of the programThe program is able to continue to operate successfullyIntended ScopePrioritize continued execution even after concrete evidence oferrorClearly might not be acceptable for all computationssafety-critical systems like air traffic control can benefitBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceScopeApproachGoalDo not necessarily restore the data structure to previousconsistent state the program was intoDeliver repaired data structures satisfying the consistencyassumptions of the programThe program is able to continue to operate successfullyIntended ScopePrioritize continued execution even after concrete evidence oferrorClearly might not be acceptable for all computationssafety-critical systems like air traffic control can benefitBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceScopeApproachBasic ApproachData structure viewsConcrete view – in memory bitsAbstract view – relations between abstract objectsspecification of high level constraintsreasoning to repair inconsistenciesSpecificationSet of model definition rulesSet of consistency constraintsBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceScopeApproachAutomatic toolGenerate algorithm that builds the model,Inspect the model and data structures to find constraintviolationsRepair data structuresRepair algorithmInconsistency detectionConverts each violated constraint to DNF (disjunctive normalform)Apply repair actions – may cause other constraint to beviolatedBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceScopeApproachAutomatic toolGenerate algorithm that builds the model,Inspect the model and data structures to find constraintviolationsRepair data structuresRepair algorithmInconsistency detectionConverts each violated constraint to DNF (disjunctive normalform)Apply repair actions – may cause other constraint to beviolatedBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceScopeApproachInvoking Check & RepairData structures are updated, may be inconsistent temporarilyProgrammer marks program points where he/she expects datastructures to be consistentAugment programs to perform check & repair in signalhandlersPersistent data structures – use a stand alone separatemechanismBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceModel ConstructionConsistency ConstraintsAn example, FATFigure: Inconsistent File SystemFigure: Repaired File SystemBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceModel ConstructionConsistency ConstraintsFAT ConstraintsChain Disjointness: Each block should be in at most onechainFree Block Consistency: No chain should contain a blockmarked as freeAbstract ConstraintsDeveloper specifies a translation from concrete data structurerepresentation to abstract modelExpress the constraints in terms of the abstract modelBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceModel ConstructionConsistency ConstraintsFAT ConstraintsChain Disjointness: Each block should be in at most onechainFree Block Consistency: No chain should contain a blockmarked as freeAbstract ConstraintsDeveloper specifies a translation from concrete data structurerepresentation to abstract modelExpress the constraints in terms of the abstract modelBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check & RepairExperienceModel ConstructionConsistency ConstraintsObject and Relation Declarationsset blocks of integer : partition used | free;relation next : used -> used;blocksusedfreeFigure: Graphical Representation of Object and Relation DeclarationsBrian Demski, Martin Rinard Automatic Detection and Repair of Errors in Data StructuresIntroductionExampleSpecification Language, Check &


View Full Document

CORNELL CS 612 - Automatic Detection and Repair of Errors in Data Structures

Download Automatic Detection and Repair of Errors in Data Structures
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Automatic Detection and Repair of Errors in Data Structures and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Automatic Detection and Repair of Errors in Data Structures 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?