Preview

Моделирование и анализ информационных систем

Расширенный поиск

Автоматическое обнаружение ошибок конкурентной модификации данных в моделях на языке SystemC

Аннотация

Модели систем на языке SystemC, как правило, являются параллельными программами и поэтому могут содержать ошибки синхронизации. Одним из типов ошибок синхронизации являются ошибки конкурентной модификации данных.
В данной статье предлагается подход к обнаружению ошибок конкурентной модификации данных в моделях на языке SystemC на основе статического анализа. Разработаны алгоритмы, обеспечивающие анализ программ на языке SystemC без количественного времени. Эти алгоритмы позволяют обнаружить все ошибки конкурентной модификации данных, имеющиеся в программе. Эффективность предложенного подхода подтверждается экспериментальными исследованиями разработанного средства обнаружения ошибок на наборе тестовых программ.

Об авторах

Алексей Владимирович Захаров
Санкт-Петербургский государственный политехнический университет
Россия


Михаил Юрьевич Моисеев
Санкт-Петербургский государственный политехнический университет
Россия


Список литературы

1. -2005 IEEE Standard SystemC Language Reference Manual.

2. Savage S., Burrows M. et al. Eraser: a Dynamic Data Race Detector for Multithreaded Programs //J. ACM Transaction of Computer System. 1997. 15. P. 391-411.

3. Pierre L., Ferro L. Enhancing the Assertion-based Verification of TLM Designs with Reentrancy // 8th International Conference on Formal Methods and Models for Codesign. 2010. P. 103-112.

4. Blanc N., Kroening D. Race Analysis for SystemC using Model Checking // ICCAD. 2008. P. 356-363.

5. Traulsen C., Cornet J., Moy M., Maraninchi F. A SystemC/TLM Semantics in Promela and Its Possible Applications // 14th Workshop on Model Checking Software SPIN. 2007. P. 204-222.

6. Garavel H., Helmstetter C., Ponsini O., Serwe W. Verification of an Industrial SystemC/TLM Model Using LOTOS and CADP // 7th IEEE/ACM International Conference on Formal Methods and Models for Co-Design. 2009. P. 46-55.

7. Hojjat H., Mousavi M.R., Sirjani M. Process Algebraic Verification of SystemC Codes // 8th International Conference on Application of Concurrency to System Design. 2008. P. 62-67.

8. Zhang Yu, Vedrine F., Monsuez B. SystemC Waiting-State Automata // 1st International Workshop on Verification and Evaluation of Computer and Communication Systems. 2007.

9. Pratikakis P., Foster J.S., Hicks M. LOCKSMITH: Practical Static Race Detection for C // J. ACM Transactions on Programming Languages and Systems. 2011.

10. Kahlon V., Sankaranarayanan S., Gupta A. Semantic Reduction of Thread Interleavings in Concurrent Programs // 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2009.

11. Kahlon V., Sinha N., Kruus E., Zhang Y. Static Data Race Detection for Concurrent Programs with Asynchronous Calls // 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering. 2009.

12. Terauchi T. Checking Race Freedom via Linear Programming // ACM SIGPLAN conference on Programming language design and implementation. 2008.

13. Naik M., Aiken A. Conditional Must Not Aliasing for Static Race Detection // 34th annual ACM SIGPLAN-SIGACT symposium on POPL. 2007.

14. Itsykson V.M., Moiseev M.Ju., Zakharov A.V. et al. Automatic Defects Detection in Industrial C/C++ Software // 5th Central and Eastern European Software Engineering Conference in Russia. 2009.

15. Aegis Error Detection Tool. <http://www.digiteklabs.ru/aegis/>


Рецензия

Для цитирования:


Захаров А.В., Моисеев М.Ю. Автоматическое обнаружение ошибок конкурентной модификации данных в моделях на языке SystemC. Моделирование и анализ информационных систем. 2011;18(4):94-105.

For citation:


Zakharov A.V., Moiseev M.J. Automatic Data Race Error Detection in SystemC Models. Modeling and Analysis of Information Systems. 2011;18(4):94-105. (In Russ.)

Просмотров: 402


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)