TY - GEN
T1 - Accumulation Analysis
AU - Kellogg, Martin
AU - Shadab, Narges
AU - Sridharan, Manu
AU - Ernst, Michael D.
N1 - Publisher Copyright:
© Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst; licensed under Creative Commons License CC-BY 4.0
PY - 2022/6/1
Y1 - 2022/6/1
N2 - A typestate specification indicates which behaviors of an object are permitted in each of the object's states. In the general case, soundly checking a typestate specification requires precise information about aliasing (i.e., an alias or pointer analysis), which is computationally expensive. This requirement has hindered the adoption of sound typestate analyses in practice. This paper identifies accumulation typestate specifications, which are the subset of typestate specifications that can be soundly checked without any information about aliasing. An accumulation typestate specification can be checked instead by an accumulation analysis: a simple, fast dataflow analysis that conservatively approximates the operations that have been performed on an object. This paper formalizes the notions of accumulation analysis and accumulation typestate specification. It proves that accumulation typestate specifications are exactly those typestate specifications that can be checked soundly without aliasing information. Further, 41% of the typestate specifications that appear in the research literature are accumulation typestate specifications.
AB - A typestate specification indicates which behaviors of an object are permitted in each of the object's states. In the general case, soundly checking a typestate specification requires precise information about aliasing (i.e., an alias or pointer analysis), which is computationally expensive. This requirement has hindered the adoption of sound typestate analyses in practice. This paper identifies accumulation typestate specifications, which are the subset of typestate specifications that can be soundly checked without any information about aliasing. An accumulation typestate specification can be checked instead by an accumulation analysis: a simple, fast dataflow analysis that conservatively approximates the operations that have been performed on an object. This paper formalizes the notions of accumulation analysis and accumulation typestate specification. It proves that accumulation typestate specifications are exactly those typestate specifications that can be checked soundly without aliasing information. Further, 41% of the typestate specifications that appear in the research literature are accumulation typestate specifications.
KW - Typestate
KW - finite-state property
UR - http://www.scopus.com/inward/record.url?scp=85134320985&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85134320985&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.ECOOP.2022.10
DO - 10.4230/LIPIcs.ECOOP.2022.10
M3 - Conference contribution
AN - SCOPUS:85134320985
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 36th European Conference on Object-Oriented Programming, ECOOP 2022
A2 - Ali, Karim
A2 - Vitek, Jan
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 36th European Conference on Object-Oriented Programming, ECOOP 2022
Y2 - 6 June 2022 through 10 June 2022
ER -