Finally, after over three years of hard work, I actually have a diploma to prove that it was all for something! Yay!
To be honest, it felt kind of anti climactic, but I guess since I missed my bachelor's graduation I might as well attend this one. The weather wasn't great, and the ceremony was kinda boring, but it was fun nonetheless, especially with my lovely fiancée Anna being my official paparazzi and taking photos all the time! :)
Make sure to checkout some of the photos she took:-
Friday, May 09, 2008
Monday, May 05, 2008
Model Checking with SPIN and Promela
As I mentioned in my previous post, one of the most valuable tools I recently discovered for debugging multithreaded applications is model checking; more specifically the Promela language and the SPIN model checker.
Promela isn't a programming language, but a modelling language that you use to describe the algorithm you'd like to model. It's quite a simple language, without many of the features that we're used to in a proper programming language such as functions, for loops, or even proper scoping of variables. At first those limitations bothered me, but what I soon learned is that those limitations are what make Promela feasible..
You see, when you write a Promela model of your algorithm, you should only focus on the high level details of the algorithm, forget about any nasty implementation details. One of the things that you should specify are correctness assertions, or the algorithm's invariants, which if violated would indicate that there's a bug in the algorithm.
After the model is ready, spin converts it into a C program, which you compile and run. Running this program constructs the state space of the system and tries to find a state that violates some of the invariants or assertions. Since the basic type of search performs an exhaustive search of literally every possible state in the system, if it doesn't find an error - then it means that your algorithm is correct! ...... ... That is assuming of course that the model and the assumptions within it are correct as well.
The thing I like the most about it is that when it finds an error, spin is capable of producing the shortest possible path to that error! In my case, while debugging my STM, this path is usually around 100 steps. That's it! So debugging a complex multithreaded algorithm is reduced to just reading these 100 or so steps and figuring out what went wrong! As easy as debugging a single-threaded application!
That said, model checking is not a silver bullet. First of all, you need to learn a new language and a new tool. Learning how to use SPIN and Promela is actually quite easy, but still that's one more thing to do before actually debugging. Also I found that the resources available online and a bit lacking. Fortunately the book The SPIN Model Checker at the library and I think it's an excellent resource.
The other thing to keep in mind is that even if the model has no errors in it, that doesn't mean that the algorithm is correct; the model itself could be wrong, the invariants or assertions specified might not be correct either. Moreover, the problem is that the more complicated the algorithm is, the bigger the state space and more time and memory are required to verify the model. This applies to increasing the number of processes in the system as well. In my case, I was only able to do exhaustive searches for three processes. Adding one more process make it completely infeasible - it requires an estimates 4 terabytes of memory to do an exhaustive search for 4 processes in my algorithm.
You could go back to theory and prove that if the model is correct for 3 processes then it's also correct for N, but until you do that you cannot be sure that it is.
Moreover, Promela only models the algorithm. Implementation issues are hidden. So memory ordering, cache coherence and performance all aren't reflected in the Promela model. You could try to account for some of these in the model, but that would just increase the state space significantly and it's still possible that you forgot something.
I did find that to be a plus though, the fact that the implementation details aren't there means that the algorithm is clearer when written in Promela than in C for example, which makes it easier to share the core algorithm with others. I guess that's why Ananian used Promela code in his PhD thesis.
Promela isn't a programming language, but a modelling language that you use to describe the algorithm you'd like to model. It's quite a simple language, without many of the features that we're used to in a proper programming language such as functions, for loops, or even proper scoping of variables. At first those limitations bothered me, but what I soon learned is that those limitations are what make Promela feasible..
You see, when you write a Promela model of your algorithm, you should only focus on the high level details of the algorithm, forget about any nasty implementation details. One of the things that you should specify are correctness assertions, or the algorithm's invariants, which if violated would indicate that there's a bug in the algorithm.
After the model is ready, spin converts it into a C program, which you compile and run. Running this program constructs the state space of the system and tries to find a state that violates some of the invariants or assertions. Since the basic type of search performs an exhaustive search of literally every possible state in the system, if it doesn't find an error - then it means that your algorithm is correct! ...... ... That is assuming of course that the model and the assumptions within it are correct as well.
The thing I like the most about it is that when it finds an error, spin is capable of producing the shortest possible path to that error! In my case, while debugging my STM, this path is usually around 100 steps. That's it! So debugging a complex multithreaded algorithm is reduced to just reading these 100 or so steps and figuring out what went wrong! As easy as debugging a single-threaded application!
That said, model checking is not a silver bullet. First of all, you need to learn a new language and a new tool. Learning how to use SPIN and Promela is actually quite easy, but still that's one more thing to do before actually debugging. Also I found that the resources available online and a bit lacking. Fortunately the book The SPIN Model Checker at the library and I think it's an excellent resource.
at the library and I think it's an excellent resource.The other thing to keep in mind is that even if the model has no errors in it, that doesn't mean that the algorithm is correct; the model itself could be wrong, the invariants or assertions specified might not be correct either. Moreover, the problem is that the more complicated the algorithm is, the bigger the state space and more time and memory are required to verify the model. This applies to increasing the number of processes in the system as well. In my case, I was only able to do exhaustive searches for three processes. Adding one more process make it completely infeasible - it requires an estimates 4 terabytes of memory to do an exhaustive search for 4 processes in my algorithm.
You could go back to theory and prove that if the model is correct for 3 processes then it's also correct for N, but until you do that you cannot be sure that it is.
Moreover, Promela only models the algorithm. Implementation issues are hidden. So memory ordering, cache coherence and performance all aren't reflected in the Promela model. You could try to account for some of these in the model, but that would just increase the state space significantly and it's still possible that you forgot something.
I did find that to be a plus though, the fact that the implementation details aren't there means that the algorithm is clearer when written in Promela than in C for example, which makes it easier to share the core algorithm with others. I guess that's why Ananian used Promela code in his PhD thesis.
Wednesday, April 30, 2008
Debugging Multithreaded Programs
A lot of my work involves writing the code for NZSTM, a software transactional memory scheme. This is in essence a multithreaded program, and anyone who's had to write a multithreaded program knows that it's not a walk in the park. The problem is that it involves reasoning about multiple things running in parallel, and all the possible interactions between them -- whereas us as human being really have a hard time keeping track of concurrent events...
Moreover, debugging tools that are used with single-threaded applications often don't work as well in a multithreaded environment. The debugger itself introduces some sense of synchronization to the program, and often when used on a multithreaded program to try and trace it the bug just disappears (heisenbug). Even debugging by printf could mess with the whole dynamics of the system therefore hiding the bug... So what to do?
I find that careful consideration of the algorithm before coding it, then making sure to code it as clearly as possible (worry about performance later), and incrementally is one of the most important factors. Make sure to unit-test all different components of the algorithm if possible, and whenever you change something perform a regression test to make sure that it's still working fine. In a way this solutions sounds a lot like saying that to loose weight all you have to do is eat less and exercise more -- easier said than done.
That said, some bugs just won't go away! What can you do at that point?
First off, make sure that you use your assertions. Almost at every point where you can make a meaningful assertion about the state of the system do apply it. This is really helpful in narrowing down where the problem is before it actually manifests itself in other ways (i.e. crashing or producing incorrect results). Plus, adding assertions is also good as a method of self-documenting the code; a person who reads the code knows what the state of the system should (or shouldn't) be at that point.
Second thing I use is trace buffers; basically you preallocate a part of memory and store certain messages rather than printing them. It's sort of like debugging by printf except that the messages are stored in the buffer rather than printed to the screen, and you can dump the buffer after the program finishes or if it crashes (by catching the signal). Using that method still could alter the dynamics of your code, but it's less invasive than debugging by printf since printfs are quite expensive, while using a trace buffer is significantly cheaper. A nice article that talks more about trace buffers can be found in Dr. Dobbs Journal.
The last element in my debugging toolbox is model checking, in my case using SPIN and Promela. I've heard about model checking a while back and I've used it in the context of Computer Architecture (Verilog). It never occurred to me that it could help me until I read C. S. Ananian's work, where he also uses model checking.
Now that I've used Promela, I've found it to be the best tool for debugging multithreaded programs. I'll write a separate entry on Promela later. But for the time being suffice it to say that I'd recommend this tool for anyone writing even mildly complicated parallel programs.
Keep in mind though that all of these tools just help out after the fact. The most important step really is to think through the algorithm carefully and try and think through all the corner cases.
"Program testing can be used to show the presence of bugs, but never to show their absence!" -Dijkstra
Moreover, debugging tools that are used with single-threaded applications often don't work as well in a multithreaded environment. The debugger itself introduces some sense of synchronization to the program, and often when used on a multithreaded program to try and trace it the bug just disappears (heisenbug). Even debugging by printf could mess with the whole dynamics of the system therefore hiding the bug... So what to do?
I find that careful consideration of the algorithm before coding it, then making sure to code it as clearly as possible (worry about performance later), and incrementally is one of the most important factors. Make sure to unit-test all different components of the algorithm if possible, and whenever you change something perform a regression test to make sure that it's still working fine. In a way this solutions sounds a lot like saying that to loose weight all you have to do is eat less and exercise more -- easier said than done.
That said, some bugs just won't go away! What can you do at that point?
First off, make sure that you use your assertions. Almost at every point where you can make a meaningful assertion about the state of the system do apply it. This is really helpful in narrowing down where the problem is before it actually manifests itself in other ways (i.e. crashing or producing incorrect results). Plus, adding assertions is also good as a method of self-documenting the code; a person who reads the code knows what the state of the system should (or shouldn't) be at that point.
Second thing I use is trace buffers; basically you preallocate a part of memory and store certain messages rather than printing them. It's sort of like debugging by printf except that the messages are stored in the buffer rather than printed to the screen, and you can dump the buffer after the program finishes or if it crashes (by catching the signal). Using that method still could alter the dynamics of your code, but it's less invasive than debugging by printf since printfs are quite expensive, while using a trace buffer is significantly cheaper. A nice article that talks more about trace buffers can be found in Dr. Dobbs Journal.
The last element in my debugging toolbox is model checking, in my case using SPIN and Promela. I've heard about model checking a while back and I've used it in the context of Computer Architecture (Verilog). It never occurred to me that it could help me until I read C. S. Ananian's work, where he also uses model checking.
Now that I've used Promela, I've found it to be the best tool for debugging multithreaded programs. I'll write a separate entry on Promela later. But for the time being suffice it to say that I'd recommend this tool for anyone writing even mildly complicated parallel programs.
Keep in mind though that all of these tools just help out after the fact. The most important step really is to think through the algorithm carefully and try and think through all the corner cases.
"Program testing can be used to show the presence of bugs, but never to show their absence!" -Dijkstra
Sunday, April 27, 2008
Picasa 2.7 for Linux and More Photos!
I just got around to installing Picasa 2.7 for Linux. It's still a bit rough around the edges but it's getting there. One feature that finally made it to the Linux version is the ability to upload photos! Yay! This means it's now way easier to upload photos to my Picasa album....
Therefore, I went all crazy and uploaded photos of a bunch of stuff Anna and I have been doing since we got back to New Zealand this year. Check them out and let me know what you think...
Therefore, I went all crazy and uploaded photos of a bunch of stuff Anna and I have been doing since we got back to New Zealand this year. Check them out and let me know what you think...
Friday, April 25, 2008
Scandinavia and Shanghai Photos
So, I finally got around to uploading some photos of my trip to Scandinavia; where I went to meet up with Anna (my fiance) and her family. I also visited good old Stefan in Stockholm, met up with Ninna there. Unfortunately it was quite a quick trip. I also managed to go to Gothenburg and give a talk, then got some sort of food poisoning or stomach flu! But I recovered quickly.
Then a quick trip to Copenhagen on the way to Shanghai, where we met up with Phoebe. Finally, back to Auckland where the PhD work was waiting...
Anyway, click on the album links below to checkout the photos!
Then a quick trip to Copenhagen on the way to Shanghai, where we met up with Phoebe. Finally, back to Auckland where the PhD work was waiting...
Anyway, click on the album links below to checkout the photos!
Thursday, April 24, 2008
Geocaching for Linux
I'm into geocaching. It combines my love of the wild outdoors with my geeky side! I now actually have an excuse to muck around with a GPS device! Anyhow, I'm also a Linux user. The problem is, geocaching.com's "send to garmin" feature unsurprisingly doesn't work on Linux. So I wrote a script in Python that takes cache waypoint numbers (e.g. GCVWMR) as parameters and sends the info to your garmin, along with a truncated hint. I learned Python while writing this script, so apologies for any weirdnesses therein. :)
This humble script is under the GPL3. But it would be nice if you could email me with any comments you have regarding how it works. I would also appreciate comments about my actual code (style for example).
Important: make sure to read geocaching.com's terms of use and don't use the script in any way that might violate those terms.
I've only tested this script using my Garmin eTrex Venture with a USB cable. You must have gpsbabel installed since my script uses it to actually send the data. Also you need to edit the script and enter your username and password since that's the only way to get the coordinates for the caches.
Here's the script: geo.py
Speaking of which, my favourite caches are Hidden in the Numbers and Battlefields. Check them out if you're in Auckland.
Edit to add: I haven't done any geocaching for a really long time now, and this script probably doesn't work. Leaving this here for historical reasons.
About Me
I am a hardworking Ph.D. student in Computer Science at the University of Auckland, New Zealand, doing research on Computer Architecture and Transactional Memory under Jim Goodman.
Subscribe to:
Posts (Atom)