Я. И. Роскошный, Д. И. Цителов, В. Ю. Трифанов, Р. А. Елизаров
Цена: 50 руб.
Обнаружение гонок — актуальная задача верификации многопоточных программ. Существующие методы подразделяются на динамические, статические и смешанные. Одной из основных проблем динамических методов являются высокие накладные расходы, в частности, необходимость контролировать все обращения к разделяемым переменным, по которым возможна гонка. Для обеспечения корректной синхронизации при обращении к потенциально разделяемым переменным часто применяются устойчивые шаблонные решения. В статье рассматриваются некоторые наиболее типичные шаблоны обеспечения синхронизации доступа к разделяемым переменным и перспективы доказательства их корректности средствами статического анализа. Предложен алгоритм определения переменных защищенных во всех возможных ветвях исполнения и реализован соответствующий инструмент для языка Java. Инструмент апробирован на различных синтетических тестах и реальных программах, интегрирован с
ранее разработанным авторами динамическим детектором гонок jDRD, который был представлен на TMPA-2013.
Ключевые слова: статический анализ; поиск гонок; многопоточность; Java.
REFERENCES
1. Netzer, R.H.B. Race condition detection for debugging shared-memory parallel
programs (Ph.D. thesis, University of Wisconsin at Madison, Madison, USA). 1991.
2. Netzer, R.H.B., & Miller, B.P. What are race conditions? Some issues and
formalizations. ACM Letters on Programming Languages and Systems, 1992, Vol. 1,
No. 1, 74–88.
3. Trifanov, V., & Tsitelov, D. Dynamic data races detection in Java programs based
on synchronization contracts [Динамический поиск гонок в Java-программах на
основе синхронизационных контрактов]. Tools & Methods of Program Analysis
(TMPA-2013), 2013, pp. 273–285.
4. Whaley, J., & Rinard, M. Compositional pointer and escape analysis for java
programs. Proceedings of the 14th ACM SIGPLAN Conference on Object-Oriented
Programming, Systems, Languages, and Applications, OOPSLA '99. 2000, NY, USA,
pp. 187–206.
5. Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., & Sundaresan, V. Soot –
a java bytecode optimization framework. 1999, Proceedings Conference of the Centre
for Advanced Studies on Collaborative research, CASCON '99.
6. Bilardi, G., & Pingali, K. Algorithms for computing the static single assignment
form. Journal of the ACM (JACM), 2003, Vol. 50, No. 3, pp. 375–425.
7. Soot [A framework for analyzing and transforming Java and Android applications].
Retrieved January 15, 2016, from http://sable.github.io/soot/
8. Naik, M., Aiken, A., & Whaley, J. Effective static race detection for Java. ACM
SIGPLAN Notices, 2006, Vol. 41, No. 6, pp. 308–319.
9. Naik, M. Chord: A versatile platform for program analysis. In Tutorial at ACM
Conference on Programming Language Design and Implementation, PLDI 2011,
2011.
10. Hovemeyer, D., & Pugh, W. Finding bugs is easy. ACM SIGPLAN Notices,
2004, Vol. 39, Issue 12, pp.92–106.
11. Jtest [Parasoft Jtest: Java static analysis, code review, unit testing, runtime error
detection]. Retrieved January 15, 2016, from https://www.parasoft.com/product/jtest/
12. Coverity [Static code analysis]. Retrieved January 15, 2016, from http://www.
synopsys.com/software/coverity
13. Artho, D. Finding faults in multi-threaded programs (Master’s thesis, Institute
of Computer Systems, Swiss Federal Institute of Technology, Zurich, Switzerland).
2001.
14. ThreadSafe [A static analysis tool for finding concurrency bugs and potential
performance issues]. 2015, Edinburgh, UK: Contemplate Ltd. Retrieved January 15,
2016, from http://www.contemplateltd.com/threadsafe
15. Mamun, Md. Concurrent Software Testing: A Systematic Review and an
Evaluation of Static Analysis Tools (Master’s thesis, Blekinge Institute of Technology,
Blekinge, Sweden). 2009.
16. Spathoulas, A. Assessing Tools for Finding Bugs in Concurrent Java (Master’s
thesis, University of Edinburgh, Edinburgh, Great Britain). 2014.
17. Mamun, Md., Khanam, A., Grahn, H., & Feldt, R. Comparing four static analysis
tools for java concurrency bugs. 2010, Proceedings of the Third Swedish Workshop on
Multi-Core Computing (MCC-10). Retrieved January 15, 2016, from docplayer.net/
storage/31/15116173/1460715033/pn7P5hwpvZvIOkygyCcnVQ/15116173.pdf
18. Blanchet, B. Escape analysis for JavaTM: Theory and practice. ACM Transactions
on Programming Languages and Systems (TOPLAS), 2003, Vol. 25, Issue 6, pp. 713–
775.
19. Kotzmann, T., & Mossenbock, H. Run-time support for optimizations based on
escape analysis. 2007, Proceedings of the International Symposium on Code Generation
and Optimization (CGO'07), pp. 49–60. doi: 10.1109/CGO.2007.34
