EE392C Emerging EE392C Emerging Applications:Applications:Verification ApplicationsVerification ApplicationsApril 15, 2003April 15, 2003David BloomDavid BloomSuzanne RivoireSuzanne RivoireJohn WhaleyJohn WhaleyOutlineOutlineMotivationMotivationBeyond simulation and testingBeyond simulation and testingModel checkingModel checkingTheorem provingTheorem provingHardware supportHardware supportSummarySummaryMotivationMotivationMissionMission--critical systemscritical systemsEx. Space shuttle, medical instrumentsEx. Space shuttle, medical instrumentsComplex, expensive systemsComplex, expensive systemsEx. Telephone switching systems, arithmetic Ex. Telephone switching systems, arithmetic units in CPUunits in CPUUsed widely for both software and Used widely for both software and hardware systemshardware systemsBeyond Simulation and Beyond Simulation and TestingTestingSimulation and testing require the development Simulation and testing require the development of inputs (stimuli), and observation of outputsof inputs (stimuli), and observation of outputsOnly as good as your test casesOnly as good as your test casesAdequate for many commercial applications, but Adequate for many commercial applications, but not good enough for critical systems and suchnot good enough for critical systems and suchFormal verification exhaustively Formal verification exhaustively provesprovesthe the correctnesscorrectnessMuch more time consuming and complexMuch more time consuming and complexModel CheckingModel CheckingCreate a finite state description of a Create a finite state description of a system to be verifiedsystem to be verifiedExhaustively search the finite state Exhaustively search the finite state space to determine if a specification is space to determine if a specification is truetrue3 main steps in model checking:3 main steps in model checking:1.1.Create the modelCreate the model2.2.Specify properties that must holdSpecify properties that must hold3.3.Verify model against specificationsVerify model against specificationsModel CheckingModel CheckingVerification should always terminate with a Verification should always terminate with a true or false conditiontrue or false conditionBut, complexity of the model (number of finite But, complexity of the model (number of finite states) can explodestates) can explodeProcess of verification is automatic, but can Process of verification is automatic, but can be prohibitively longbe prohibitively longA lot of research on state reduction, which is not of A lot of research on state reduction, which is not of interest to usinterest to usBut, perhaps we can exploit parallelismBut, perhaps we can exploit parallelismModel CheckingModel CheckingLarge state space can be partitioned into Large state space can be partitioned into subspacessubspacesSubspaces can be processed in parallel Subspaces can be processed in parallel ––great for TLPgreat for TLPTend to be memory bound processes Tend to be memory bound processes ––large ratio of memory to arithmetic large ratio of memory to arithmetic instructionsinstructionsAccess patterns mostly random Access patterns mostly random ––little to no little to no locality to exploitlocality to exploitPerhaps software Perhaps software prefetchingprefetchingcan helpcan helpModel Checking Model Checking ––Case StudyCase StudyReduced Ordered Binary Decision Reduced Ordered Binary Decision Diagrams: a fundamental data Diagrams: a fundamental data structure in model checkingstructure in model checkingROBDDsROBDDsare produced through the are produced through the repeated application of:repeated application of: Redundant test elimination Equivalent sub-graph sharingWe investigated the application We investigated the application characteristics of a popular BDD characteristics of a popular BDD packagepackageBuDDyBuDDypackage version 2.2package version 2.2Compiled with Intel Compiled with Intel ––O3 compilerO3 compilerIntel P4Intel P4--2.4 GHz using 2.4 GHz using VTuneVTuneBuDDyBuDDytest cases for modeltest cases for model--checkingcheckingx1x2x2x3x40 11011100001Model Checking Model Checking ––ResultsResultsAs expected, it was almost As expected, it was almost completely memory boundcompletely memory bound80% of time was spent on 80% of time was spent on cache missescache missesCPI was 6.5CPI was 6.5Read bus utilization: 8.38%Read bus utilization: 8.38%To find equivalent nodes, To find equivalent nodes, code hashes all nodes into code hashes all nodes into a large hash tablea large hash tableTable is too large to fit into Table is too large to fit into the cache, and accesses are the cache, and accesses are randomrandomProcessor time5%74%6%5%3%7%Level 1 cacheload missesLevel 2 cacheload misses64K AliasingConflictsBlocked StoreForwardsBranchmispredictionsOtherTheorem Theorem ProversProversInductive and deductive verification Inductive and deductive verification techniquestechniquesPROS: No state explosionPROS: No state explosionCONS: It’s hard! (And requires more CONS: It’s hard! (And requires more programmer intervention)programmer intervention)Case Study: ACL2Case Study: ACL2Developed in 1989 at UTDeveloped in 1989 at UT--Austin and AMDAustin and AMDShares ancestry with Stanford’s PVSShares ancestry with Stanford’s PVSWritten in Common LispWritten in Common LispDevelop ModelVerifyTLP Opportunities in ACL2TLP Opportunities in ACL2FooBar2Bar1BazzTLPSpeculative MultithreadingMake a changeHardware support for bug Hardware support for bug detection (detection (OplingerOplinger& Lam 2002)& Lam 2002)Hardware support for fineHardware support for fine--grained transactionsgrained transactionsSoftware marks beginning of transactionSoftware marks beginning of transactionAll further sideAll further side--effects (memory and register) are effects (memory and register) are bufferedbufferedSoftware decides when to either commit or abort the Software decides when to either commit or abort the transactiontransactionUse Thread Level Speculation to parallelize Use Thread Level Speculation to parallelize monitoring codemonitoring codeVery effective because monitoring code is typically Very effective