Loading...
Please wait, while we are loading the content...
Similar Documents
Race analysis for SystemC using model checking
| Content Provider | CiteSeerX |
|---|---|
| Author | Kroening, Daniel |
| Description | SystemC is a system-level modeling language that offers a wide range of features to describe concurrent systems at different levels of abstraction. The SystemC standard permits simulators to implement a deterministic scheduling policy, which often hides concurrency-related design flaws. We present a novel compiler for SystemC that integrates a very precise formal race analysis by means of Model Checking. Our compiler produces a simulator that uses the outcome of the analysis to perform partial order reduction. The key insight to make the Model Checking engine scale is to apply it only to tiny fractions of the SystemC model. We show that the outcome of the analysis is not only valuable to eliminate redundant context switches at runtime, but can also be used to diagnose race conditions statically. In particular, our analysis is able to reveal races that can remain undetected during simulation and is able to formally prove the absence of races. |
| File Format | |
| Language | English |
| Publisher Institution | In Proceedings of ICCAD 2008. IEEE |
| Access Restriction | Open |
| Subject Keyword | Race Analysis Novel Compiler Different Level Concurrency-related Design Flaw Systemc Standard Race Condition Model Checking Engine Scale Tiny Fraction Wide Range Key Insight Redundant Context Switch Concurrent System Partial Order Reduction Model Checking Precise Formal Race Analysis Systemc Model System-level Modeling Language Deterministic Scheduling Policy |
| Content Type | Text |
| Resource Type | Article |
