Сравнительный анализ статических методов верификации динамической памяти
Аннотация
В статье дается обзор существующих методов верификации динамической памяти; проводится их сравнительный анализ; оценивается применимость для решения задач управления, контроля и верификации динамической памяти. Данная статья состоит из восьми разделов. Первый раздел - введение. Во втором обсуждаются проблемы управления динамической памятью. В третьем рассматривается исчисление Хоара. В четвёртом речь идёт о преобразованиях heap в стек. Пятый вводит понятие анализа образов динамической памяти. Шестой посвящен ротации указателей, седьмой - логике распределенной памяти. В последнем разделе рассматриваются возможные направления дальнейших научных исследований в данной области, в частности: распознавание на уровне записи различных экземпляров объектов; автоматизация доказательств; использование «горячего» кода, то есть программного кода, который сам себя обновляет при запуске программы; расширение интуитивности объяснений доказательств и другие
Литература
R. Love, Linux Kernel Development. Addison-Wesley Professional, 3rd ed., 2010.
C. A. R. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM, vol.12, no. 10, pp. 576–580, 1969.
W. E.Weihl, “Interprocedural data 2ow analysis in the presence of pointers, procedure variables and label variables,” Paul W. Abrahams, Richard J. Lipton, and Stephen R. Bourne, eds., Proc. of the 7th ACM SIGPLAN-SIGACT symp. on Principles of Programming Languages, ACM Press, pp. 83–94, 1980.
B. P. Miller, D. Koski, C. P. Lee, V. Maganty, R. Murthy, A. Natarajan, and J. Steidl, “Nichts dazugelernt—empirische studie zur zuverl¨assigkeit von unix-utilities,” iX – Magazin f¨ur professionelle Informationstechnik, no. 9, pp. 108–121, 1995.
B. P. Miller, L. Fredriksen, and B, So, “An empirical study of the reliability of unix utilities,” In Proc. of the Workshop of Parallel and Distributed Debugging, Digital Equipment Corporation, pp. 1–22. 1990.
R. Jones, A. Hosking, and Eliot Moss. The Garbage Collection Handbook: The Art of Automatic Memory Management, Chapman & Hall/CRC, 1st ed., 2011.
A. W. Appel, “Garbage collection can be faster than stack allocation,” Information Processing Letters, Elsevier North-Holland, vol. 25, no. 4, pp. 275–279, 1987.
M. Tofte and J.-P. Talpin, “Region-based memory management,” Information and Computation, vol. 132, no. 2, pp. 109–176, 1997.
B. Meyer, “Proving pointer program properties — part 2: The overall object structure,” ETH Z¨urich, Journal of Object Technology, 2003.
R. G. Larson, “Minimizing garbage collection as a function of region size,” SIAM Journal on Computing, vol. 6, no. 4, pp. 663–668, 1977.
P. Sinha, A memory-eWcient doubly linked list, [Online], Available: http://www.linuxjournal.com/ article/6828
N. Parlante, Linked list basics, document no.103 from the stanford computer science education library, 2001. [Online], Available: http://cslibrary.stanford.edu/10
R. Haberland, Tutorials and examples, no. 11, 2016. [Online], Available: https://bitbucket.org/reneH123/
R. Jones and Sun Microsystems Inc., “Memory management in the java hotspot virtual machine,” Technical Report, April 2006. [Online], Available: http://www.oracle.com/technetwork/articles/java/ index-jsp-140228.html
Iso c++ standard, n4296, Intl. Organization of Standardization, 19 Nov. 2014. [Online], Available: https://isocpp.org/1les/papers/n4296.pdf
R. Bornat. “Proving pointer programs in hoare logic,” R. Backhouse and J. N. Oliveira, eds., Proc. of the 5th Intl. Conf. on Mathematics of Program Construction, Lecture Notes in Computer Science, Springer, vol. 1, pp. 102–126, 2000.
M. Abadi and L. Cardelli, A Theory of Objects, Springer: Secaucus, New Jersey, USA, 1996.
C. A. Gunter and John C. (eds.) Mitchell. Theoretical aspects of object-oriented programming—types, semantics, and language design. MIT Press, 1994.
M. Abadi and K. Rustan M. Leino, “A logic of object-oriented programs,” In Proc. of the 7th Intl. Joint Conf. CAAP/FASE on Theory and Practice of Software Development, Springer, pp. 682–696, 1997.
H. Ehrig and B. K. Rosen, “The mathematics of record handling,” SIAM Journal on Computing, vol. 9, no. 3, pp. 441–469, 1980.
M. Abadi, “Baby modula-3 and a theory of object,” Technical Report SRC-RR-95, Systems Research Center, Digital Equipment Corporation, 1993.
K. Rustan M. Leino. “Recursive object types in a logic of object-oriented programs,” Nordic Journal of Computing, vol. 5, no. 4, pp. 330–360, 1998.
A. Banerjee, D. A. Naumann, and S. Rosenberg, “Regional logic for local reasoning about global invariants,” J. Vitek, ed., European conf. on Object-Oriented Programming, vol. 5142 of Lecture Notes in Computer Science, Springer, Berlin Heidelberg, pp. 387–411, 2008.
Wikipedia, Region-based memory management, [Online], Available: https://en.wikipedia.org/wiki/ Region-based_memory_management
M. Barnett, R. DeLine, M. F¨ahndrich, K. Rustan M. Leino, and W. Schulte, “Veri1cation of objectoriented programs with invariants,” Journal of Object Technology, vol. 3, no. 6, pp. 27–56, 2004.
P. M¨uller, “Modular Speci1cation and Veri1cation of Object-Oriented Programs. PhD thesis,” Fern- Universit¨at Hagen, Germany, 2002.
D. F. D’Souza and A. C. Wills, “Objects, Components, and Frameworks with UML: The Catalysis Approach. Object Technology Series,” Addison-Wesley, 1998.
Object Management Group (OMG). Object constraint language version 2.2, 2 2010. [Online], Available: http://www.omg.org/spec/OCL/2.2
S. Muchnick, Advanced Compiler Design and Implementation, Morgan Kaufmann Publishers Inc., 2007.
G. Ramalingam, “The undecidability of aliasing,” ACM Transactions on Programming Languages and Systems, vol. 16, no. 5, pp. 1467–1471, 1994.
The gnu compiler collection, [Online], Available: http://gcc.gnu.org
S. Horwitz, P. Pfeiffer, and T. Reps, “Dependence analysis for pointer variables,” In Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation, New York, USA, pp. 28–40, 1989.
U. Khedker, A. Sanyal, and Bageshri Karkare, Data Flow Analysis: Theory and Practice, 1st ed., CRC Press Inc., Boca Raton, Florida, USA, 2009.
T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms, 3rd ed., MIT Press, 2009.
R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. “EWciently computing static single assignment form and the control dependence graph,” ACM Transactions on Programming Lanuages and Systems, vol. 13, no. 4, pp. 451–490, 1991.
Static single assignment book, latest from july 2014. [Online], Available: http://ssabook.gforge.inria. fr/latest/book.pdf.electronically 37. N. A. Naeem and O. Lhot´ak. “EWcient alias set analysis using ssa form,” In Proc. Of the intl. symp. on Memory Management, New York, USA, pp. 79–88, 2009.
V. Pavlu. Shape-based alias analysis — extracting alias sets from shape graphs for comparison of shape analysis precision. Master’s thesis, Vienna University of Technology, Austria, 2010.
B. Steensgaard. “Points-to analysis in almost linear time,” In Proc. of the 23rd ACM SIGPLAN-SIGACT symp. on Principles of Programming Languages, New York, USA, pp. 32–41, 1996
K. R. Apt. “Ten years of hoare’s logic: A survey — part I,” ACM Transactions on Programming Languages and Systems, vol. 3, no. 4, pp. 431–483, 1981.
E. M. Jr. Clarke, “Programming language constructs for which it is impossible to obtain good hoare axiom systems,” Journal of the ACM, vol. 26, no. 1, pp. 29–147, New York, USA, 1979.
K. R. Apt and E.-R. Olderog, “Veri1cation of sequential and concurrent programs,” SIAM Review, vol. 35, no. 2, pp. 330–331, 1993.
S. Cook, “Soundness and completeness of an axiom system for program veri1cation,” SIAM Journal on Computing, vol. 1, pp. 70–90, 1978.
R. Stansifer, “Presburger’s article on integer airthmetic: Remarks and translation. Technical Report TR84-639,” Computer Science Department, Cornell University, 1984.
B. Meyer, “Proving pointer program properties,” ETH Z¨urich, Journal of Object Technology, 2003.
N. D. Jones and Steven S. Muchnick, “Even simple programs are hard to analyze,” In Proc. Of 2nd ACM SIGACT-SIGPLAN symp. on Principles of Programming Languages, pp. 106–118, 1975.
M. Sagiv, T. Reps, and Reinhard Wilhelm, “Parametric shape analysis via 3-valued logic,” ACM Transactions on Programming Languages and Systems, vol. 24, no. 3, pp. 217–298, 2002.
F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis, Springer Berlin, Heidelberg, 1999.
M. Hind, “Pointer analysis: Haven’t we solved this problem yet?,” USA IBM Watson Research Center, ed., In Proc. of the ACM SIGPLAN-SIGSOFT workshop on Program Analysis for Software Tools and Engineering, pp. 54–61. ACM, 2001.
S. A. Parduhn, R. Seidel, and R. Wilhelm. “Algorithm visualization using concrete and abstract shape graphs,” In Proc. of the ACM symp. on Software Visualization, pp. 33–36, 2008.
C. Calcagno, D. Distefano, P. O’Hearn, and H. Yang. “Compositional shape analysis by means of biabduction,” In Proc. of the 36th annual ACM SIGPLAN-SIGACT symp. on Principles of Programming Languages, vol. 36, pp. 289–300, 2009.
N. Suzuki. “Analysis of pointer rotation,” Communications of the ACM, vol. 25, no. 5, pp. 330–335, 1982.
J. C. Reynolds, “Separation logic: A logic for shared mutable data structures,” In Proc. Of the 17th Annual IEEE symp. on Logic in Computer Science, pp. 55–74,Washington, DC, USA, 2002.
J. Berdine, C. Calcagno, and P. W. O’Hearn, “Symbolic execution with separation logic,” In 3rd Asian symp. on Programming Languages and Systems, pp. 52–68, Tsukuba, Japan, 2005.
J. C. Reynolds. An Introduction to Separation Logic, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA, 2009. course book. [Online], Available: http://www.cs.cmu.edu/afs/cs.cmu.edu/ project/fox-19/member/jcr
R. M. Burstall, “Some techniques for proving correctness of programs which alter data structures,” In Bernard Meltzer and Donald Michie, ed., Machine Intelligence, Edinburgh University Press, Scotland, vol. 7, pp. 23–50. 1972.
M. Parkinson and G. Bierman, “Separation logic and abstraction,” SIGPLAN Notes, vol. 40, no. 1, pp. 247–258, 2005.
G. Restall. Introduction to Substructural Logic. Routledge Publishing, 2000.
C. Hurlin. Speci1cation and Veri1cation of Multithreaded Object-Oriented Programs with Separation Logic. PhD thesis, Universit´e Nice — Sophia Antipolis, France, 2009.
M. J. Parkinson. Local Reasoning for Java. PhD thesis, Cambridge University, England, 2005.
M. Dodds. Graph Transformations and Pointer Structures. PhD thesis, University of York, England, 2008.
Материал публикуется под лицензией:
