Detecting and Escaping Infinite Loops with Jolt
In the research conducted by Michael Carbin, Sasa Misailovic, Michael Kling, and Martin Rinard at the Massachusetts Institute of Technology, a solution for detecting and escaping infinite loops using Jolt was proposed. This innovative approach aims to automatically recognize and exit infinite loops, preventing program crashes and data loss. By incorporating Jolt into the program execution process, developers can enhance user experience by ensuring uninterrupted workflow and output generation, even in the presence of infinite loops.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Detecting and Escaping Infinite Loops with Jolt Michael Carbin with Sasa Misailovic, Michael Kling, and Martin Rinard Massachusetts Institute of Technology
Our Research Context Researcher Developer User
Motivation You run a program Edit a document Search for a keyword Indent source code files Program infinite loops You get no output You lose your work
Our Solution: J lt Automatically detect and escape infinite loops Program produces output User doesn t lose work Logo courtesy J.D. Rhoades
Basic Approach 1. Compile program with Jolt compiler. (adds instrumentation to mark loop boundaries) 2. Execute program. 3. Program stops responding. 4. Launch Jolt monitor. Monitor takes snapshots at each loop head. If two snapshots are same, infinite loop! 5. Jolt jumps to instruction after loop.
Does this work? 1. Are real infinite loops this simple? 2. Does Jolt produce a safe execution? 3. Does Jolt produce better output than Ctrl-C? 4. Does Jolt match the developer s fix? 5. Can this be implemented efficiently?
Infinite Loop in Grep conf.in grep E [0-9]* --color=always conf.in 25th ECOOP v2.5 v2.5.1 stdout 25th ECOOP Infinite Loop
Infinite Loop in Grep 2.5 regex *beg 25th ECOOP [0-9]* regex *beg 25th ECOOP [0-9]* 1: void prline(regex_t regex, char *beg) { 3: while (true) { 4: int size = 0; 5: int off = match(regex, beg, &size); 6: if (off == -1) { 7: break; 8: } 9: char const *b = beg + off; 10: fwrite(beg, 1, off, stdout); 11: enable_color(); 10: fwrite (b, 1, size, stdout); 11: disable_color(); 11: beg = b + size; 12: } 14: } 2 0 size off regex *beg 25th ECOOP [0-9]* regex *beg [0-9]* th ECOOP 2 6 25th ECOOP 2 0 size off size 25th ECOOP *b off *b regex *beg [0-9]* th ECOOP 0 0 25th ECOOP regex *beg th ECOOP [0-9]* size 0 0 size off off *b th ECOOP *b
Step 1: Compile Grep Jolt Compiler Adds instructions that mark loop boundaries.
Jolt Compiles Grep 1: void prline(regex_t regex, char *beg) { 2: 3: 4: while (true) { 5: 6: int size = 0; 7: int offset = match(regex, beg, &size); 8: if (offset == -1) { 9: 10: break; 11: } 12: char const *b = beg + offset; 13: fwrite (b, sizeof (char), size, stdout); 14: beg = b + size; 15: } 16: 17: } 18:
Jolt Compiles Grep 1: void prline(regex_t regex, char *beg) { 2: 3: jolt_loop_entry(ID); 4: while (true) { 5: jolt_loop_body(ID, &jolt_escape_dest); 6: int size = 0; 7: int offset = match(regex, beg, &size); 8: if (offset == -1) { 9: jolt_loop_exit(ID); 10: break; 11: } 12: char const *b = beg + offset; 13: fwrite (b, sizeof (char), size, stdout); 14: beg = b + size; 15: } 16: jolt_escape_dest: 17: 18: }
Step 2: Run Grep Grep runs as normal. Control instrumentation overhead ~2.5%.
Step 3: Grep stops Responding Grep enters infinite loop, does not respond!
Step 4: Launch Jolt Monitor Jolt dynamically attaches to grep Monitors execution Jolt Computes snapshot at each loop head If two snapshots are the same, infinite loop!
How to Compute a Snapshot Efficiently 1. Log all registers and memory addresses that each loop iteration accesses. 2. Record the contents of these registers and addresses at the head of the loop.
Comparing Two Snapshots Snapshot 1 First, check if snapshots have the same accessed Registers and Memory addresses Next check if contents of Accessed registers and Accessed memory addresses are the same regex [0-9]* beg 0xdeadbeef *beg th ECOOP 0 size 0 off b 0xdeadbeef th ECOOP *b Snapshot 2 regex [0-9]* beg 0xdeadbeef *beg th ECOOP 0 size 0 off b 0xdeadbeef th ECOOP *b
Step 5: Jolt Exits the Loop 1: void prline(regex_t regex, char *beg) { 2: jolt_loop_entry(ID); 3: while (true) { 4: jolt_loop_body(ID, &jolt_escape_dest); 5: int size = 0; 6: int offset = match(regex, beg, &size); 7: if (offset == -1) { 8: jolt_loop_exit(ID); 9: break; 10: } 11: char const *b = beg + offset; 12: fwrite (b, sizeof (char), size, stdout); 13: beg = b + size; 14: } 15: jolt_escape_dest: 16: }
Output Jolt Ctrl-C
Does this work for Grep? Is it safe? Yes, no side-effects (except on output files). Is it better than Ctrl-C? Yes, continues to match additional lines and files. Is it equivalent to the correct fix? Yes, corrected by break if size is 0 (v2.5.1). 3 years later no, v2.5.3 skips all size 0 matches. 25th ECOOP 11
5 Applications and 8 Infinite Loops 1. ctags : line numbers of functions in code. v5.5 : one loop in fortran module. v5.7b : one loop in python module. 2. grep (v2.5): matches regexp against files (3 loops). 3. ping (v20100214): icmp utility. 4. indent (v1.1-svr 4): indents source code. 5. look (v1.9.1): matches a word against dictionary file.
Question #1 Are infinite loops this simple? Benchmark ctags-f ctags-p grep ping look indent Detected Yes Yes Yes Yes Yes No 7 of 8
Question #2 Does escape produce a safe execution? Methodology Validated execution with Valgrind and by hand. Tested over available infinite loop triggering inputs. Results Yes, side effects often localized = consistent state. Or, simple correctness invariants.
Question #3 Does Jolt produce a better output than Ctrl-C? Methodology Defined output abstraction, and compared outputs. Results Yes, errors often isolated to single output unit (e.g., file). Example indent: correct indention resumes on next file. Terminating indent deletes your source code!!! Development hint: don t update files in-place.
Question #4 Does escape model the developers fix? Methodology Manually inspected a later version of each application. Results ctags: no, output semantically different on some inputs. grep: jolt matches fix for two of three loops (3 years). ping, indent, look: yes, in all cases. Example ping: developer used continue instead of break.
Question #5 Can this be implemented efficiently? Benchmark Overhead (%) Detection(s) ctags-f 7.3 ctags-p 5.2 grep 2.5 ping 1.6 look 0.0 indent 8.4 0.319 0.334 0.551* 0.287 0.296 x *Average over the three loops
Observations Infinite loops can (and often do) frustrate users. Infinite loops can be (and often are) simple. Errors are localized in some cases. Jolt s results can be (and often are) better than no results at all. Applying Jolt can (and often does) model the developer s fix.
Did We Just Solve the Halting Problem? No
Limitations Jolt doesn t detect infinite loops that always change state. Though still possible to exit loop if user desires. We did not consider busy-wait loops. Though a good question is what does it mean when a user thinks a program is waiting too long?
Future Work Off-the-shelf binaries - pure dynamic analysis Safety guarantees shepherded execution Larger classes of loops - symbolic non- termination analysis
Related Work Bounding Loop Length Detecting and Eliminating Memory Leaks Using Cyclic Memory Allocation (Nguyen and Rinard, ISMM 07) Non-termination Provers TNT (Gupta, et al.) using Invariant Generation (POPL 08) Looper (Burnim, et al.) using Symbolic Execution (ASE 09) Termination Provers Terminator (Cook, et al.) (PLDI 06)
Takeaway Jolt gives users another option to deal with programs that infinite loop. Another hammer in the toolbox to help users deal with otherwise fatal errors.
Thank You/Questions? From: "Armando Solar-Lezama" <asolar@csail.mit.edu> To: "Martin Rinard" <rinard@csail.mit.edu> Subject: Thanks I was writing a document in Word this morning, and after about an hour of unsaved work, Word went into an infinite loop that made the application completely frozen. So, having listened to your talks too many times, I got my debugger, paused the program, changed the program counter to a point a few instructions past the end of the loop, and let it keep running from there. Word went back to working as if nothing had ever happened. I was able to finish my document, save it, and close Word without problems. So thanks, Armando.
Bug Reports grep indent 1994 ctags 2.5 -- 13 Mar 2002 2.5.1 -- 29 Oct 2004 2.5.3 -- 02 Aug 2007 5.5 2003 5.7b 2007
Instrumentation Overhead Bench. Average Lowest Highest 1.073 1.068 1.08 ctags-f 1.052 1.035 1.057 ctags-p 1.025 1.014 1.028 grep 1.016 1.005 1.024 ping 1 1 1 look 1.084 1.082 1.086 indent
Detection Time Bench. Time (s) Footprint (b) Length 0.319 240 256 ctags-f 0.334 312 992 ctags-p 0.585 992 4030 grep-c 0.579 992 4036 grep-cc 0.490 846 2506 grep-m 0.287 192 54 ping 0.296 300 378 look
