TY - GEN
T1 - Contextual effects for version-consistent dynamic software updating and safe concurrent programming
AU - Neamtiu, Iulian
AU - Hicks, Michael
AU - Foster, Jeffrey S.
AU - Pratikakis, Polyvios
PY - 2008
Y1 - 2008
N2 - This paper presents a generalization of standard effect systems that we call contextual effects. A traditional effect system computes the effect of an expression e. Our system additionally computes the effects of the computational context in which e occurs. More specifically, we computethe effect of the computation that has already occurred(the prior effect) and the effect of the computation yet to take place (the future effect). Contextual effects are useful when the past or future computation of the program is relevant at various program points. We present two substantial examples. First, we show how prior and future effects can be used to enforce transactional version consistency(TVC), a novel correctness property for dynamic software updates. TV Censures that programmer-designated transactional code blocks appear to execute entirely at the same code version, even if a dynamic update occurs in the middle of the block. Second, we show how future effects can be used in the analysis of multi-threaded programs to find thread-shared locations. This is an essential step in applications such as data race detection.
AB - This paper presents a generalization of standard effect systems that we call contextual effects. A traditional effect system computes the effect of an expression e. Our system additionally computes the effects of the computational context in which e occurs. More specifically, we computethe effect of the computation that has already occurred(the prior effect) and the effect of the computation yet to take place (the future effect). Contextual effects are useful when the past or future computation of the program is relevant at various program points. We present two substantial examples. First, we show how prior and future effects can be used to enforce transactional version consistency(TVC), a novel correctness property for dynamic software updates. TV Censures that programmer-designated transactional code blocks appear to execute entirely at the same code version, even if a dynamic update occurs in the middle of the block. Second, we show how future effects can be used in the analysis of multi-threaded programs to find thread-shared locations. This is an essential step in applications such as data race detection.
KW - computation effects
KW - contextual effects
KW - data race detection
KW - dynamic software updating
KW - type and effect systems
KW - version consistency
UR - http://www.scopus.com/inward/record.url?scp=84865662465&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84865662465&partnerID=8YFLogxK
U2 - 10.1145/1328438.1328447
DO - 10.1145/1328438.1328447
M3 - Conference contribution
AN - SCOPUS:84865662465
SN - 9781595936899
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 37
EP - 49
BT - POPL'08 - Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
T2 - 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'08
Y2 - 7 January 2008 through 12 January 2008
ER -