I received overwhelmingly positive feedback. Below I share some of the comments about TLA+ and the paper review assignments. (I removed the flattering feedback about my teaching, while I enjoyed reading them. I put a lot of effort in my teaching and I am happy when the students recognize how much I care. That keeps me motivated.)
Feedback about using TLA+I assigned two TLA+ projects. The first project was modeling Voldemort key-value store with client-side routing, and the second project was about extending the first with chain-replication and server-side routing. I had given the students TLA+ demonstrations in a couple classes, and shared with them PlusCal modeling of several of the distributed algorithms I covered in the class.
(I had wrote about how and why I decided to integrate TLA+ to my distributed systems class in a couple earlier posts including: Using TLA+ for teaching distributed systems, My experience with using TLA+ in distributed systems class. I also posted several TLA+/PlusCal modeling of distributed algorithms in my blog. You can reach all of my posts about TLA+/PlusCal here.)
Most of the students mentioned that they appreciated the TLA+ projects. The students said TLA+ showed them how tricky distributed algorithms can get, and without TLA+ they wouldn't be able to figure out the intricacies of those algorithms.
TLA+ is a great tool to learn to use if you're planning on pursuing a career in computer science. Its raw ability to detect flaws in algorithms is unparalleled. I am very pleased with having been introduced to it through this class. Of all my takeaways from the class through the semester the opportunity to become familiar with this is the one I believe will help me the most in my future.
Working on the TLA+ projects taught me the most. Sitting in the classroom and going through the whole algorithm gave me an insight of the algorithm but I realized the depth of the algorithm, the problems related to it and the capability of the algorithm only when I worked on the projects.
TLA seems to be a fantastic way to reason about systems and I really enjoyed using it for the class. I aspire to use TLA+/formal verification all along my career when I get an opportunity.
I liked the invariant based way of reasoning about the correctness of a program. I liked the expressiveness of PlusCal to model complex distributed algorithms with very short lines of code.
At the same time, many students complained about the learning curve of TLA+, and that they had to spent a lot of time figuring the ropes. They said that it would help if I had arranged for more TLA+ demonstrations, and if I had assigned them some smaller projects to get them warmed up with TLA+.
I found the element of the class I really had to put a lot of time into was reading the PlusCal manual and the Dynamic help in the eclipse toolbox. There was a great deal of functionality in this programming environment I didn't know how to properly use until the end of the semester. I think the class can greatly benefit from more in depth classes or recitations on TLA+ from the syntax of PlusCal to the options and tools in the model checker.
Regarding the projects, I really enjoyed learning TLA and PlusCal and I really liked building Voldemort and Voldchain. The caveat consists in that sometimes it was difficult and frustrating, but I learned a new way of thinking programmatically and mathematically, and it was very satisfying.
Initially, I needed a lot of time to get acquainted to the PlusCal syntax. But once I got used to it, things stared flowing smoothly. I realized that TLA+ does force the designers to clearly describe and understand the design before they actually write the executable code for it. Since TLA+ has numerous benefits and advantages I hope it gets widely adopted in the industry.
The code translate check cycle was sometimes very long. To be fair this was usually a problem with the code itself or using too much state to design the model.
Some errors were very difficult to comprehend and debug in TLC model checker. Some error messages were cryptic.
I like this suggestion from one of the students. It is an ambitious idea for an introductory distributed systems course with limited time and much ground to cover, but it would be a great improvement if we can pull that off.
It would be great if the project could be a semester long one, where in the first half we design a distributed algorithm and verify its consistency properties using TLA+ and in the second half we do an implementation of the system in a high-level programming language (like Java or C++).
Reviewing papersI assigned 6 homework this semester, 4 of which involved reviewing research papers about the topics we covered. Many students commented that they didn't like reading/reviewing papers at first, but then started to find the reviewing assignments useful and enjoyable.
I just needed something to force me to do it [review papers] a few times before I could get the hang of it. Considering how much the industry changes and the absolute need to continue learning from others in the filed I think this will help me later in my career.
Because of this course I have started reading research papers on a regular basis, just because I like reading them now.
I really enjoyed the paper reviews we did. After reading the papers and writing the reviews, I actually felt like I had a thorough understanding for the content of the papers, which was a very cool feeling. Before this class, I have never read an academic paper and felt like I actually understood it.
Looking back, I am so glad that I had the opportunity to review the papers. At first I was intimidated, and didn't want to do it, but I feel much more confident and familiar with reading and evaluating research papers as a result. Part of the reason is that you posted information on how to go about this process, and it really helped to have a good method for performing this function. It also helped to know that I'm not the only one who doesn't understand the paper on the first or second pass. That you for your honesty.
I think this last student is referring to my "How I read a research paper" post.
Other commentsFavorite distributed algorithms for my students have been Paxos, hygienic dining philosophers, and Dijkstra's stabilizing token ring algorithms.
Almost all of the students mentioned that they liked the reenacting of the algorithms on the board, and those made the algorithms memorable and more easily understandable. The students all seemed to benefit from the YouTube videos I show at the beginning of lectures.
I loved the fact that the Professor showed YouTube videos in every lecture. Although at times it took me a few minutes to understand how the videos connected to the topic at hand (especially the one with Mr. Miyagi and the karate kid).
This comment was particularly interesting.
I appreciated that the professor would like to share his thinking processes with us. That was really helpful for me. As for a beginner stepping in this area, I lack the proper mind in considering the problems in distributed systems. However, professor was always offering his logic to us. That was what I could take it into my life with the knowledge I learned from the course.
I am intrigued that the student was able to catch this. Once I had wrote a post about why we should be talking more about our thought processes.
Teaching is hard work, it has its ups and downs, but looking back on the semester, I am very proud to have raised another batch of distributed systems geeks.