Race analysis for systemC using model checking
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...
| Autori principali: | , |
|---|---|
| Natura: | Journal article |
| Pubblicazione: |
Association for Computing Machinery
2010
|
| _version_ | 1826264871222640640 |
|---|---|
| author | Blanc, N Kroening, D |
| author_facet | Blanc, N Kroening, D |
| author_sort | Blanc, N |
| collection | OXFORD |
| 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. |
| first_indexed | 2024-03-06T20:14:48Z |
| format | Journal article |
| id | oxford-uuid:2bc57cf4-ee8f-441a-8cdb-a563fd5eb2d6 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T20:14:48Z |
| publishDate | 2010 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:2bc57cf4-ee8f-441a-8cdb-a563fd5eb2d62022-03-26T12:33:04ZRace analysis for systemC using model checkingJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:2bc57cf4-ee8f-441a-8cdb-a563fd5eb2d6Symplectic Elements at OxfordAssociation for Computing Machinery2010Blanc, NKroening, DSystemC 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. |
| spellingShingle | Blanc, N Kroening, D Race analysis for systemC using model checking |
| title | Race analysis for systemC using model checking |
| title_full | Race analysis for systemC using model checking |
| title_fullStr | Race analysis for systemC using model checking |
| title_full_unstemmed | Race analysis for systemC using model checking |
| title_short | Race analysis for systemC using model checking |
| title_sort | race analysis for systemc using model checking |
| work_keys_str_mv | AT blancn raceanalysisforsystemcusingmodelchecking AT kroeningd raceanalysisforsystemcusingmodelchecking |