DOC PREVIEW
Stanford CS 295 - Study Notes

This preview shows page 1-2-3 out of 9 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

CS295 FinalSpring 2009• Don’t forget to put your name and SID on this cover sheet.• Solutions will be graded on correctness and clarity. Each problem has a relatively simple and straight-forward solution. You may get as few as 0 points for a question if your solution is far more c omplicatedthan necessary. Partial solutions will be graded for partial credit.• This exam is due at no on on Tuesday, June 9. You may return the exam either by email to the coursestaff account or physically in 411 Gates (just put the exam under the door if it is closed).• If wish to ask questions during the period of the exam, please send email to the course staff [email protected]. Do not use the class newsgroup to discuss or ask questionsabout the exam.• In accordance with both the letter and spirit of the Honor Code, you will neither give nor receive assistanceon this examination.Problem Max points Points1 302 303 304 305 20TOTAL 140NAME:SID:11. SWAT vs. Saturn (30 points)SWAT and Saturn both provide memory leak detection, though one is a dynamic tool and the other isstatic. This problem asks you to compare the capabilities of the two tools. You should be able to answerall of these questions with 1-2 sentences—no essays are required!• Describe two different kinds of memory leaks that SWAT would catch, but that Saturn would not.• Describe a leak Saturn would catch, but that SWAT would not.• Give an advantage of how SWAT reports leaks to the programmer over Saturn.• Give an advantage of how Saturn reports leaks to the programmer over SWAT.22. Lock Analysis (30 points)In lecture we saw many examples of static tools that report single thread lock errors, meaning instanceswhere a single thread locks or unlocks a lock twice in a row. Indicate whether each of CQual (the versionfrom the 2002 paper) , Saturn, and BLAST would report a false positive on each of the following examples,and why. Assume in each example that x is initially unlocked.• foo() {lock(x);y += 1;unlock(x);}• mylock() { lock(x); }myunlock() {unlock(x); }foo() {mylock();y += 1;myunlock()}• foo(boolean b) {if (b) { lock(x) }y += 1;if (b) { unlock(x) }}3• mylock() { lock(x); }myunlock() {unlock(x); }foo(boolean b) {if (b) { mylock(x) }y += 1;if (b) { myunlock(x) }}43. Model Checking (30 points)Consider an API with three operations: rock, paper, and scissors. Each kind of call may be followedby more calls of the same kind, so for example rock(); rock(); rock(); is a legal sequence of calls.Furthermore, a rock call may be followed by a paper call, a paper call may be followed by a scissors call,and a scissors call may be followed by a rock call. All legal sequences begin with a call to rock. No othersequences of calls are legal.• Draw a finite state machine distinguishing correct from incorrect sequences of calls torock/paper/scissors.• For the following program, give a minimal set of predicates that would enable BLAST to provethe program safe. You do not need to show how or whether BLAST could compute your selectedpredicates—these just need to be predicates that, if BLAST found them somehow, would enable itto prove the safety of the program. You should also briefly argue why your predicates are sufficient,but you do not need to build the reachability tree. Assume each call to the function user_input()returns a fresh boolean value entered by the user.i = 0;j = 0;k = 0;do {rock();i++;while (user_input()) {rock();i++;}while (j < i) {paper();j++;}scissors();while ((k < j) && user_input()) {scissors();k++;}} while (k < i);5• Answer the same question as above for this slightly different program:i = 0;j = 0;k = 0;do {rock();i++;while (user_input()) {rock();i++;}paper();while (j < i) {paper();j++;}scissors();while ((k < j) && user_input()) {scissors();k++;}} while (k < i);• And once more for another variation:i = 0;j = 0;k = 0;do {rock();i++;while (user_input()) {rock();i++;}while (j < i) {paper();j++;}while (k < j) {scissors();k++;}} while (k < i);64. Annotation-Based Systems (30 points)Consider the following code:void bubble_sort(char * p, int len) (1){int i, j; (2)char temp; (3)char *end = p + len; (4)char *ptr = p; (5)for(i = 1; ptr + i < end; ++i) { (6)for(j = len - 1; j >= i; --j) { (7)if(ptr[j-1] >= ptr[j]) { (8)temp = ptr[j-1]; (9)ptr[j-1] = ptr[j]; (10)ptr[j] = temp; (11)}}}}• What annotations are needed to compile this code with Deputy? Show the annotation and the linenumber. You may, if you wish, use Deputy to answer this question (but it is not required that youdo so).• How could you use DAIKON to infer Deputy annotations? Sketch an algorithm for automaticallyproducing the Deputy annotations from one or more runs of DAIKON and Deputy.75. Miscellaneous Short Answer (30 points)• Many bug finding systems convert loops to loop-free code by replacing each loop with just the(unrolled) first few iterations of the loop. Given an example of a class of bugs for which this strategyworks well and a c lass of bugs for which this strategy works poorly.• Consider the following piece of code:void func(int i, int j) {char *p1;char *p2;p1 = malloc(BUFFER_SIZE);if (j >= i) {p2 = malloc(BUFFER_SIZE);if (i >= j) {p2 = p1;}free(ptr2);}free(ptr1);}What bug is present in this code and which tools (static or dynamic) that we discussed in lectureshould find it?• What is the difference between bug finding and verification? Name one advantage and one disad-vantage of each.8• Consider the following idea: Take the predicates reported by Cooperative Bug Isolation as beinghighly likely to generate a crash and give them as assumptions to a BLAST-like model checker (i.e.,BLAST only considers program states where the predicates are true). The goal is then to see ifBLAST can produce real counterexample (crashing) traces using these predicates. Clearly this ideawill sometimes work; briefly, what is one class of circumstances in which it might not


View Full Document

Stanford CS 295 - Study Notes

Download Study Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Study Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Study Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?