Formal Guarantees for Localized Bug Fixes: A Methodological Review
This review delves into a formal method for verifying bug fixes, specifically focusing on ensuring robustness and scalability in bug identification and classification. The OpenSPARC Story unfolds a methodology for bug fix verification, emphasizing bug resurfacing prevention and fix classification based on simulated data inputs. Detailed steps for slice computation and weakest precondition analysis are highlighted, culminating in the categorization of bug fixes into robust and clean fixes or identifying those that may still persist. Experimental results and case scenarios are presented to illustrate the efficacy of the proposed bug fix verification approach.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
2012/10/12 Formal Guarantees for Localized Bug Fixes TCAD Review 1
Outline Introduction The OpenSPARC Story Methodology Outline Detailed Methodology Slice Computation Weakest Pre-condition (WP) along a slice Bug Fix Classification Experimental Results 2012/10/12 2
Introduction A formal method for verifying the robustness of the bug fix w.r.t. the specific buf More Scalable than BMC 2012/10/12 Test bench Design New Simulation Properties Exist Bugs Proposed Mehod Classify Bug fix Fix Bug 3
The OpenSPARC Story Hand-shaking between writeback buffer(WB) and miss buffer (MB) Normal working scenario Request misses in the L2 cache, then the request is stored in MB Search address in WB queue, and wbHit is enabled if hit the data turn of trueMissFlag dramWrAck is true if data writeback successfully WB enables depEn and sends MB entry number depMbid[3:0] to wake up corresponding entry 2012/10/12 4
The OpenSPARC Story The bug scenario Do not enable wbHit when address is hit in WB true miss (trueMissFlag turns on) evictFlag is turned on and MB sends the request to DRAM Get the wrong data from DRAM (correct data is in the WB) The property @ (posedge rclk) (wbCamHit == 1) |=> ## 5 (!dramRdReq) wbCamHit indicates that the requested address is found in WB, then the read request dramRdReq should not be high 5 cycles after that 2012/10/12 5
Methodology Outline Given test-bench TB, fixed implementation D and the property P 1. Simulate D with TB to find the start/finish time cycle 2. Re-simulate D with TB to dump the statements S executed between the start/finish time 3. Construct a dynamic causal slice C from S to isolate all statements which affect the success of P 2012/10/12 6
Methodology Outline 4. Compute unrestricted weakest precondition Q along the slice 5. Categorize the bug fix into three types Robust/Clean fix Type 2: bug cannot resurface with different data input on the same control path as simulated by the given TB Type 3: bug is not fixed 2012/10/12 7
Slice Computation Identifying the slicing window The slicing window w.r.t. a bug-fix assertion P is a finite time interval [a:b] s.t. the start match point of the antecedent of P is a, and the end match point of the corresponding evaluation attempt of the consequent is b Ex. Assertion: a ##1 b |-> ##1 c ##1 c 2012/10/12 8 Slicing window = [3:6]
Slice Computation Identifying the causal slice Dump list of statements, along with the time cycle at which they were executed Two rules For all variables appearing in P, we dump their values at the start match point For each clock cycle between the start and end match points of P, we unconditionally dump all executed statements along with the clock cycle 2012/10/12 9
Slice Computation Backward dynamic slicing computation Start from the time-annotated variable with the highest time cycle. Ex. dramRdReq Check dynamic data dependencies Check dynamic control dependencies 2012/10/12 Eliminated <t1+4, L3> 10 <t1+4, L4> <t1+4, L5> <t1+5, L1>
Weakest pre-condition along a slice Two rules Data dependency: For a statement of the form x=e, we use wp(x = e, Q) : Q[e/x] Control dependency: For a control statement involving the condition R, we use wp(R, Q) : R /\ Q Example WP(<t1+5, L1>, !dramRdReq) = WP(<t1+4, L5>, !dramPick) = WP(<t1+4, L4>, !dramPickPrev) = WP(<t1+4, L3>, !dramPickPrev /\ dramPkEn ) 2012/10/12 11
Bug Fix Classification Analysis the WP computed form the dynamic slice Type-1/Robust fix: WP will come out to be a constant Example 2012/10/12 WP = !(!wbCamHit /\ dramPick) = !0 (since initial value wbCamHit = 1) 12
Bug Fix Classification Type-2 WP returns an expression where the conjunct that comes from the post-condition c becomes a tautology, but some inputs to the causal trace remain behind in the conjuncts which were derived from the control dependencies and for differing valuations of these inputs, other control flows can manifest. Example WP = !0 /\ dramPkEn /\ enbl = dramPkEn /\enbl Enbl and dramPkEn can take different valuations in other runs 2012/10/12 13
Bug Fix Classification Type-3 Fix is not able to eliminate the bug entirely even for this control flow exercised by the given test bench Return a conunterexample 2012/10/12 14
Experimental Results Cache coherence test case of Pentium Pro Property: 2012/10/12 20 cycles 15
Experimental Results OpenSPARC L2 cache control logic test case Statistics of L2 cache control logic of OpenSPARC 2012/10/12 Result (OOM: out of memory) 16
