TY - GEN
T1 - Efficient Incrementalized Runtime Checking of Linear Measures on Lists
AU - Gyori, Alex
AU - Garg, Pranav
AU - Pek, Edgar
AU - Madhusudan, P.
N1 - This research was partially supported by the NSF Grant Nos. CCF-1138994, CCF-1421503, CCF-1527395, and CNS-1646305.
PY - 2017/5/15
Y1 - 2017/5/15
N2 - We present mechanisms to specify and efficiently check, at runtime, assertions that express structural properties and aggregate measures of dynamically manipulated linkedlist data structures. Checking assertions involving the structure, disjointness, and aggregation measures on lists and list segments typically requires linear or quadratic time in the size of the heap. Our main contribution is an incrementalization instrumentation that tracks properties of data structures dynamically as the program executes and leads to orders of magnitude speedup in assertion checking in many scenarios. Our incrementalization incurs a constant overhead on updates to list structures but enables checking assertions in constant time, independent of the size of the heap. We define a general class of functions on lists, called linear measures, which are amenable to our incrementalization technique. We demonstrate the effectiveness of our technique by showing orders of magnitude speedup in two scenarios: one scenario stemming from assertions at the level of APIs of list-manipulating libraries and the other scenario stemming from providing dynamic detection of security attacks caused by malicious rootkits.
AB - We present mechanisms to specify and efficiently check, at runtime, assertions that express structural properties and aggregate measures of dynamically manipulated linkedlist data structures. Checking assertions involving the structure, disjointness, and aggregation measures on lists and list segments typically requires linear or quadratic time in the size of the heap. Our main contribution is an incrementalization instrumentation that tracks properties of data structures dynamically as the program executes and leads to orders of magnitude speedup in assertion checking in many scenarios. Our incrementalization incurs a constant overhead on updates to list structures but enables checking assertions in constant time, independent of the size of the heap. We define a general class of functions on lists, called linear measures, which are amenable to our incrementalization technique. We demonstrate the effectiveness of our technique by showing orders of magnitude speedup in two scenarios: one scenario stemming from assertions at the level of APIs of list-manipulating libraries and the other scenario stemming from providing dynamic detection of security attacks caused by malicious rootkits.
KW - Assertion Checking
KW - Incrementalization
KW - Runtime Verification
UR - http://www.scopus.com/inward/record.url?scp=85020741202&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85020741202&partnerID=8YFLogxK
U2 - 10.1109/ICST.2017.35
DO - 10.1109/ICST.2017.35
M3 - Conference contribution
AN - SCOPUS:85020741202
T3 - Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017
SP - 310
EP - 320
BT - Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017
Y2 - 13 March 2017 through 17 March 2017
ER -