A static analysis to detect re-entrancy in object oriented programs

We are interested in object-oriented programming methodologies that enable static verification of object-invariants. Reasoning soundly and effectively about the consistency of objects is still one of the main stumbling blocks to pushing object-oriented program verification into the mainstream. More...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Garbervetsky, Diego
Publicado: 2008
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16601769_v7_n5_p5_Fahndrich
http://hdl.handle.net/20.500.12110/paper_16601769_v7_n5_p5_Fahndrich
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_16601769_v7_n5_p5_Fahndrich
record_format dspace
spelling paper:paper_16601769_v7_n5_p5_Fahndrich2023-06-08T16:25:40Z A static analysis to detect re-entrancy in object oriented programs Garbervetsky, Diego We are interested in object-oriented programming methodologies that enable static verification of object-invariants. Reasoning soundly and effectively about the consistency of objects is still one of the main stumbling blocks to pushing object-oriented program verification into the mainstream. More precisely, any sound methodology must be able to guarantee that the invariant of the receiver object holds at all method call sites. Establishing this proof obligation is tedious, and instead programmers would like to reason informally as follows: methods should be able to assume that the object invariant holds on entry, as long as all constructors establish it, and all methods guarantee that the receiver invariant holds on exit. This reasoning is only correct under certain conditions. In this paper we present sufficient conditions that make reasoning as above sound and show how these conditions can be checked separately, allowing us to divide the verification problem into two well-defined parts: 1) reasoning about object consistency of the receiver within a single method, and 2) reasoning about the absence of inconsistent re-entrant calls. In particular, when reasoning about the object consistency of the receiver within a method, our approach does not require proving invariants on other objects whose methods are called. We present a novel whole program analysis to determine the absence of inconsistent re-entrant calls. It warns developers when re-entrant calls are made on objects whose invariants may not hold. The analysis augments a points-to analysis to compute potential call chains in order to detect re-entrant calls. Fil:Garbervetsky, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2008 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16601769_v7_n5_p5_Fahndrich http://hdl.handle.net/20.500.12110/paper_16601769_v7_n5_p5_Fahndrich
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
description We are interested in object-oriented programming methodologies that enable static verification of object-invariants. Reasoning soundly and effectively about the consistency of objects is still one of the main stumbling blocks to pushing object-oriented program verification into the mainstream. More precisely, any sound methodology must be able to guarantee that the invariant of the receiver object holds at all method call sites. Establishing this proof obligation is tedious, and instead programmers would like to reason informally as follows: methods should be able to assume that the object invariant holds on entry, as long as all constructors establish it, and all methods guarantee that the receiver invariant holds on exit. This reasoning is only correct under certain conditions. In this paper we present sufficient conditions that make reasoning as above sound and show how these conditions can be checked separately, allowing us to divide the verification problem into two well-defined parts: 1) reasoning about object consistency of the receiver within a single method, and 2) reasoning about the absence of inconsistent re-entrant calls. In particular, when reasoning about the object consistency of the receiver within a method, our approach does not require proving invariants on other objects whose methods are called. We present a novel whole program analysis to determine the absence of inconsistent re-entrant calls. It warns developers when re-entrant calls are made on objects whose invariants may not hold. The analysis augments a points-to analysis to compute potential call chains in order to detect re-entrant calls.
author Garbervetsky, Diego
spellingShingle Garbervetsky, Diego
A static analysis to detect re-entrancy in object oriented programs
author_facet Garbervetsky, Diego
author_sort Garbervetsky, Diego
title A static analysis to detect re-entrancy in object oriented programs
title_short A static analysis to detect re-entrancy in object oriented programs
title_full A static analysis to detect re-entrancy in object oriented programs
title_fullStr A static analysis to detect re-entrancy in object oriented programs
title_full_unstemmed A static analysis to detect re-entrancy in object oriented programs
title_sort static analysis to detect re-entrancy in object oriented programs
publishDate 2008
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16601769_v7_n5_p5_Fahndrich
http://hdl.handle.net/20.500.12110/paper_16601769_v7_n5_p5_Fahndrich
work_keys_str_mv AT garbervetskydiego astaticanalysistodetectreentrancyinobjectorientedprograms
AT garbervetskydiego staticanalysistodetectreentrancyinobjectorientedprograms
_version_ 1768542335705022464

Ejemplares similares