CS 586

valgrind output

For full credit, valgrind should report 0 errors, 0 bytes definitely lost and 0 bytes in use at exit. If you compile your program with -ggdb valgring will give you line numbers and function names for memory leak locations.

An example of acceptable valgrind output is...
[jones@flute tmp]$ valgrind --leak-check=yes ./a.out
==7046== Memcheck, a.k.a. Valgrind, a memory error detector for x86-linux.
==7046== Copyright (C) 2002-2003, and GNU GPL'd, by Julian Seward.
==7046== Using valgrind-20030725, a program supervision framework for x86-linux.
==7046== Copyright (C) 2000-2003, and GNU GPL'd, by Julian Seward.
==7046== Estimated CPU clock rate is 1001 MHz
==7046== For more details, rerun with: -v
==7046==
==7046==
==7046== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
==7046== malloc/free: in use at exit: 0 bytes in 0 blocks.
==7046== malloc/free: 3 allocs, 3 frees, 84 bytes allocated.
==7046== For counts of detected errors, rerun with: -v
==7046== No malloc'd blocks -- no leaks are possible.

While the following would have some points deducted:

[jones@flute tmp]$ valgrind --leak-check=yes ./a.out
==6942== Memcheck, a.k.a. Valgrind, a memory error detector for x86-linux.
==6942== Copyright (C) 2002-2003, and GNU GPL'd, by Julian Seward.
==6942== Using valgrind-20030725, a program supervision framework for x86-linux.
==6942== Copyright (C) 2000-2003, and GNU GPL'd, by Julian Seward.
==6942== Estimated CPU clock rate is 999 MHz
==6942== For more details, rerun with: -v
==6942==
==6942==
==6942== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
==6942== malloc/free: in use at exit: 2600 bytes in 2 blocks.
==6942== malloc/free: 2 allocs, 0 frees, 2600 bytes allocated.
==6942== For counts of detected errors, rerun with: -v
==6942== searching for pointers to 2 not-freed blocks.
==6942== checked 4550036 bytes.
==6942==
==6942== LEAK SUMMARY:
==6942== definitely lost: 0 bytes in 0 blocks.
==6942== possibly lost: 0 bytes in 0 blocks.
==6942== still reachable: 2600 bytes in 2 blocks.
==6942== suppressed: 0 bytes in 0 blocks.
==6942== Reachable blocks (those to which a pointer was found) are not shown.
==6942== To see them, rerun with: --show-reachable=yes
==6942==

valgrind and the STL

[valgrind faq (see Q14)] If you are using the STL and get 'still reachable' memory at the end of your program, even though you shouldn't, then you are probably suffering from memory pooling. Memory pooliing is a feature, not a bug, in the STL implementations. For a good discussion see the faq entry above. To eliminate the reachable memory, force the compiler to use malloc and free. You can do this by setting the GLIBCPP_FORCE_NEW environment variable by doing export GLIBCPP_FORCE_NEW=1 (or similar depending on your shell).

I will have GLIBCPP_FORCE_NEW set in my environment when I compile and check your stuff. Thanks to Micah Lewis for asking the question.

How to use valgrind

Recall that CS 586 projects must not have memory leaks to get full credit. I've install a memory debugger in /users/faculty/jones/bin. Its called valgrind. To use it, run
valgrind --leak-check=yes --leak-resolution=high < program and args >

Useful BDD references

In addition to our text, you might peruse the following... [Catherine Dochy's BDD Guide, Slides by Armin Biere (most likely), starting at page 33, CAD of VLSI at the Technion by A. Kolodny, start about page 5]

Final changes to project one (due Monday 9/29)

Project 1 has been modified to reflect the changes we made in class. Whew. Its due by midnight Monday, which really means Tueday morning around 8am. Good luck and keep asking questions about the project as they come up...

Move office hours 9/25

My office hours for Thursday morning need to be moved back to 130-230 pm rather than 10-11am. Other times are available by appointment.

Homework for Friday 9/26

Translate a verse (or equivalent) from the religious text of your choice to CTL*. Due at the beginining of class Friday 9/26.

Project 1 public methods modified

Added a constructor that takes the name of a file containing a Kripke structure, deleted the read_kripke method and refined the definition of the next_states and propositions interfaces.
[Project 1]

Added "read_kripke" method to Proj. 1

[Project 1 from the syllabus] We need a public method for reading in a Kripke from a file. The function takes a filename, and creates a Kripke structure from the file. I’ll check your projects by writing a wrapper that uses your public methods to read and analyze your Kripke structure. That method will be:
void read_kripke (file *filename);
I've updated the syllabus to reflect the change

CTL* Formulas for Friday

Two formulas that describe correct behaviors of mutex protocols.

Example Kripke data files

Simple Kripke
Loop Kripke
Boring Kripke

Project 1 Clarification

The format of files containing Kripke structures has been clarified. The clarification is "there may be one or more lines beginning with “Transitions” that identify transitions. Similarly, there may be one or more lines beginning with “Label.” Each “Label” line contains one state and a list of atomic proposition (AP) labels for that state. No white space in strings used as APs, no commas between transition pairs an white space is ok everywhere else."
[Project 1 Description (from syllabus)]

States, state formulae and labels

What's the difference between a state, a state formula and a label? A state is a container for labels, a state formula is a predicate (ie, a function that returns true or false) on states and a label is an adjective that describes states. We'll go over this a little on Wednesday just to make sure its all clear.

Schedule Change

We aren't going to spend another week on Kripke Structures. We will spend some time talking about the Kripke Structure parser, but that's it. We will start into temporal logics today or Wednesday. The reading will move up so that you should start reading chapter 3 now. I'll make the third homework due this Friday though (write a specification for a mutual exclusion protocol). The Kripke parser will remain where due next Friday (Sept 26).

Homework for Friday Sept 19

Translate the behavior of two processes using Mutex1 into a Kripke structure. Find two traces in the Kripke Structure: one that allows two processes to enter the critical section and one that starves a process from access to the critical section. Turn in your traces only. Do not turn in, or even write (if you don't have to), the entire Kripke Structure. Due Friday, September 19 at the start of class.

FutureBus+ Errors

The book mentions the application of BDD-based model checking to verifying parts of the FutureBus+ protocol (page 7). This is an impressive early result. Interestingly, another paper that appeared in 1996 (4 years later) found additional deadlocks in the different configurations of the same protocol. I bring this up to emphasize that the identification of errors depends on assumptions about the system under test.
[A Platform for Combining Deductive with Algorithmic Verification - Pnueli, Shahar (ResearchIndex)]

Free Pizza, Sept 24

C.S. Fall Pizza Social is scheduled for Wed. Sept 24th and is for all students in our Fundamentals/Computer Science Major program. Tickets for the event can be obtained from the secretaries in our office.

Formal Methods class at the U of Utah

[CS 6110] This is a class taught by my PhD advisor, Ganesh Gopalakrishnan. The class covers some of the same topics as we will, but Ganesh is taking a different approach. His class will study appliations of formal methods, then use model checking (and other) tools, and finally learn the theory. We, in CS 586, are going to learn why to apply formal methods first, then learn some theory, then implement the algorithms and we may learn to use some of the tools later. I postponed learning the tools because I think that if you understand the algorithms, you can learn the tools more quickly on your own. Understanding the algorithms is harder than learning to use a tool. The advantage of Ganesh' approach is that you see the algorithms in action before you learn the theory which may help you learn the theory better.

Ambiguous Notions of Correctness

I hope you felt uncomfortable with the ambiguity in today's class. The next month of 586 is all about precise languages for defining correctness. The concept of ambiguity in correctness has a religious parallel in The Book of Mormon (and possibly other books?). See Alma 42:17-23 and 2 Nephi 2:13. I don't understand the parallel enough to write it, but the notion of a law and a definite right and wrong is fundamental.

But what about the quality?

Note the veiled frustration from the Microsoft engineer toward the end. Perhaps customers are starting to care about quailty more than deadlines? Or perhaps engineers want customers to care about quality more than deadlines?

iTnews: A Longhorn delay? Not quite

Mutex Homework

Your job is decide if they are both correct, one incorrect and the other correct or they are both correct. You should make your decision then write a position page defending your decision. On Friday, September 5, we will discuss your progress so far. The position page is due in class on Wednesday, September 10.
You’ll be graded on whether or not you made the correct decision and how you justified your decision. I hope you’ll be brutally honest in how you arrived at your conclusion.

[Mutual Exclusion]