maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1101Research ArticleОригинальные статьиArticlesАвтоматическое обнаружение ошибок конкурентной модификации данных в моделях на языке SystemCAutomatic Data Race Error Detection in SystemC ModelsЗахаровАлексей ВладимировичZakharovA. V.zakharov@kspt.ftk.spbstu.ruМоисеевМихаил ЮрьевичMoiseevM. J.mikhail.moiseev@gmail.comСанкт-Петербургский государственный политехнический университетRussian Federation20112012201118494105Copyright © Захаров А.В., Моисеев М.Ю., 20112011Захаров А.В., Моисеев М.Ю.Zakharov A.V., Moiseev M.J.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1101

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

Hardware/software systems simulated by using the SystemC language are usually parallel and, therefore, may contain synchronization errors. One widespread type of synchronization errors is data races. In this paper we propose an approach to data race detection in SystemC programs which is based on the source code static analysis. We have developed some static analysis algorithms that can extract information for data race detection in a SystemC program without quantitative time. These algorithms can detect all the errors that exist in the program. The efficiency of our approach is shown by the evaluation results of the developed tool on a set of test SystemC programs.

статический анализошибки конкурентной модификации данныхSystemCstatic analysisdata error race detectionReferences-2005 IEEE Standard SystemC Language Reference Manual.-2005 IEEE Standard SystemC Language Reference Manual.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.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.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.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.Blanc N., Kroening D. Race Analysis for SystemC using Model Checking // ICCAD. 2008. P. 356-363.Blanc N., Kroening D. Race Analysis for SystemC using Model Checking // ICCAD. 2008. P. 356-363.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.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.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.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.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.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.Zhang Yu, Vedrine F., Monsuez B. SystemC Waiting-State Automata // 1st International Workshop on Verification and Evaluation of Computer and Communication Systems. 2007.Zhang Yu, Vedrine F., Monsuez B. SystemC Waiting-State Automata // 1st International Workshop on Verification and Evaluation of Computer and Communication Systems. 2007.Pratikakis P., Foster J.S., Hicks M. LOCKSMITH: Practical Static Race Detection for C // J. ACM Transactions on Programming Languages and Systems. 2011.Pratikakis P., Foster J.S., Hicks M. LOCKSMITH: Practical Static Race Detection for C // J. ACM Transactions on Programming Languages and Systems. 2011.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.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.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.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.Terauchi T. Checking Race Freedom via Linear Programming // ACM SIGPLAN conference on Programming language design and implementation. 2008.Terauchi T. Checking Race Freedom via Linear Programming // ACM SIGPLAN conference on Programming language design and implementation. 2008.Naik M., Aiken A. Conditional Must Not Aliasing for Static Race Detection // 34th annual ACM SIGPLAN-SIGACT symposium on POPL. 2007.Naik M., Aiken A. Conditional Must Not Aliasing for Static Race Detection // 34th annual ACM SIGPLAN-SIGACT symposium on POPL. 2007.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.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.Aegis Error Detection Tool. <http://www.digiteklabs.ru/aegis/>Aegis Error Detection Tool. <http://www.digiteklabs.ru/aegis/>

The authors declare that there are no conflicts of interest present.