OOPSLA 2016 was in Amsterdam this week. Each day of the conference, one of my students presented his work:
On Wednesday, Pavel Panchekha presented "Automated Reasoning for Web Page Layout". To create a good-looking HTML webpage, it is necessary to use CSS styling. Pavel's Cassius system takes as input a picture or mockup of a webpage, and it outputs a CSS stylesheet that will produce the given layout. This is one application of a formalization of CSS that can be used not just for synthesis of CSS code, but also for automated verification and debugging.
On Thursday, Konstantin Weitz presented "Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver". BGP is a networking protocol that determines how packets are routed through the internet. ISPs configure their routers with BGP configurations, with the aim of providing good service, making a profit, satisfying contractual obligations, and not disrupting other parts of the Internet. The Bagpipe tool verifies these properties, and it found multiple errors in real-world BGP configurations.
On Friday, Calvin Loncaric presented "A Practical Framework for Type Inference Error Explanation". Type inference is famous for being a powerful way to relieve programmers of the burden of writing types, and is equally famous for giving misleading error messages, often in the wrong part of the program, when the program contains an error. Calvin's work shows a way to improve the error messages that are produced by type inference.
If you missed the conference, then be sure to check out their papers!
Friday, November 4, 2016
Wednesday, October 12, 2016
Nothing is better than the Optional type
JDK 8 introduced the
The Web and blogosphere are full of claims that the
When your code throws a
(These criticisms aren't specific to Java's implementation of
The
I have written an article that expands on the above points and offers a better solution. Here is the outline of that article:
Optional class, a container that is either empty or contains a non-null value.Optional has numerous problems without countervailing benefits. Optional does not make your code more correct or robust. There is a real problem that Optional tries to solve, and there is a better way to solve it. Therefore, you are better off using a regular possibly-null Java reference, rather than using Optional.The Web and blogosphere are full of claims that the
Optional class solves the problem of null pointer exceptions. This is not true. Changing your code to use the Optional class has these effects:- It transforms a
NullPointerExceptioninto aNoSuchElementException, which still crashes your program. - It creates new problems that were not a danger before.
- It clutters your code.
- It adds both space and time overheads.
When your code throws a
NullPointerException into a NoSuchElementException, the underlying logic bug is that you forgot to check all possibilities when processing data. It's best to use a tool that guarantees you don't forget. That helps you to understand and fix the underlying problem.(These criticisms aren't specific to Java's implementation of
Optional. Other languages that claim to have solved the problem have also merely transformed it into a different manifestation.)The
Optional class isn't all bad: if you have to use Optional, it defines methods for reducing code clutter when dealing with possibly-present data. However, you should still avoid the Optional class.I have written an article that expands on the above points and offers a better solution. Here is the outline of that article:
- Changing the exception that is thrown doesn't fix the defect or improve the code
Optionalis prone to misuseOptionalclutters your codeOptionalintroduces overhead- The real problem: remembering to perform checks
Optional's handy methods- Counterarguments
- Summary
Friday, September 30, 2016
Applying for a graduate fellowship
It is the season to apply for graduate fellowships, with the first deadline for most students being the NSF Graduate Research Fellowship.
I maintain a webpage with advice about applying for a fellowship. I have recently updated it, and you may find it useful when you apply. Good luck!
I maintain a webpage with advice about applying for a fellowship. I have recently updated it, and you may find it useful when you apply. Good luck!
Monday, September 26, 2016
JavaOne 2016 talks
I first spoke at JavaOne in 2008, and I have presented most years since. It's a great way to communicate a message about practical software development tools. An academic can even squeeze in a few few nuggets of theory as enrichment, so long as the fundamentals of usefulness to practitioners is covered.
Last week, I gave three talks (together with Werner Dietl), spanning 4 hours, at JavaOne 2016. The common theme was the use of Java 8's type annotations feature to improve code quality. This was the most rewarding year yet: with ever-increasing adoption of Java 8, there was lively interest and the sessions were very interactive with lots of questions and comments.
The slides are now available (though you always get more from being at the talk, hearing the spiel, and seeing the demos):
Tutorial TUT3422: Preventing Errors Before They Happen
Conference talk CON5739: Disciplined Locking: No More Concurrency Errors
Birds-of-a-feather session BOF3427: Using Type Annotations to Improve Your Code
Last week, I gave three talks (together with Werner Dietl), spanning 4 hours, at JavaOne 2016. The common theme was the use of Java 8's type annotations feature to improve code quality. This was the most rewarding year yet: with ever-increasing adoption of Java 8, there was lively interest and the sessions were very interactive with lots of questions and comments.
The slides are now available (though you always get more from being at the talk, hearing the spiel, and seeing the demos):
Tutorial TUT3422: Preventing Errors Before They Happen
Conference talk CON5739: Disciplined Locking: No More Concurrency Errors
Birds-of-a-feather session BOF3427: Using Type Annotations to Improve Your Code
Thursday, September 22, 2016
Predicting the 2016 presidential election
My "data programming" class, UW CSE 160, is a popular introductory computer science class. Its examples and assignments are taken from the real world and use datasets from science, engineering, business, etc. -- not from abstract math, puzzles, or programming itself, such as computing the Fibonacci sequence or implementing a linked list. These real-world examples are more compelling to students, and they better prepare students for the programming they will do in the future. The class's assignments can also be integrated into an existing class without fully adopting the methodology of real-world examples.
One particularly popular assignment asks students to predict the outcome of the 2012 election, based on polling data. Preceding the 2012 election, many political pundits, working from their gut feel, predicted a Romney win or said the election was "too close to call". Nate Silver of the website FiveThirtyEight had been predicting an Obama win for months, and he correctly predicted the outcome of every state.
The key to Silver's approach is to combine different polls using a weighted average. In a normal average, each data point contributes equally to the result. In a weighted average, some data points contribute more than others. Silver examined how well each polling organization had predicted previous elections, and then weighted their polls according to their accuracy: more biased pollsters had less effect on the weighted average.
The concepts are simple enough for beginning programmers to complete successfully after just 3 or 4 weeks of instruction. The assignment is interesting enough to be assigned later in the term, too. Since most of the assignment is provided and students just have to implement 10 functions, this assignment also gives students practice in the critical skill of reading code.
When this assignment was first handed out in January 2013, the 2012 election was a fresh memory. Now it may seem dated to students. Therefore, you could update the assignment to use polling data for the 2016 election.
Doing so requires collecting and cleaning polling data. You can find information about how we collected and cleaned data for the 2008 and 2012 elections, in file https://courses.cs.washington.edu/courses/cse140/13wi/homework/hw3/raw-data.zip. (Students: this doesn't give any hints about how to solve the assignment.)
If you adapt the Python programs in that zip file and collect polling information about the 2016 election, please share the fruits of your labor by emailing me. Other instructors and their students will appreciate it!
One particularly popular assignment asks students to predict the outcome of the 2012 election, based on polling data. Preceding the 2012 election, many political pundits, working from their gut feel, predicted a Romney win or said the election was "too close to call". Nate Silver of the website FiveThirtyEight had been predicting an Obama win for months, and he correctly predicted the outcome of every state.
The key to Silver's approach is to combine different polls using a weighted average. In a normal average, each data point contributes equally to the result. In a weighted average, some data points contribute more than others. Silver examined how well each polling organization had predicted previous elections, and then weighted their polls according to their accuracy: more biased pollsters had less effect on the weighted average.
The concepts are simple enough for beginning programmers to complete successfully after just 3 or 4 weeks of instruction. The assignment is interesting enough to be assigned later in the term, too. Since most of the assignment is provided and students just have to implement 10 functions, this assignment also gives students practice in the critical skill of reading code.
When this assignment was first handed out in January 2013, the 2012 election was a fresh memory. Now it may seem dated to students. Therefore, you could update the assignment to use polling data for the 2016 election.
Doing so requires collecting and cleaning polling data. You can find information about how we collected and cleaned data for the 2008 and 2012 elections, in file https://courses.cs.washington.edu/courses/cse140/13wi/homework/hw3/raw-data.zip. (Students: this doesn't give any hints about how to solve the assignment.)
If you adapt the Python programs in that zip file and collect polling information about the 2016 election, please share the fruits of your labor by emailing me. Other instructors and their students will appreciate it!
Friday, September 9, 2016
Python evaluation rules
You cannot program in a programming language if you don't understand how the language works. Some novices find programming a frustrating, opaque endeavor because they don't understand how the computer executes their programs. When their program does not work, they make wild guesses about what changes might improve the program, and they try out their guesses by running the program.
If a programmer understands the language, then the programmer can understand what the program is doing and why it is producing the observed output. The programmer can determine a proper fix or devise meaningful experiments to better understand what values are being manipulated at run time.
Unfortunately, not all students are taught these simple, effective techniques. I have been horrified to see instructors (even at my own institution!) teach bad habits by telling students, "The only way to know what this program does is to run it." Many programming textbooks and websites are just as bad: they don't explain the programming model, or they do so in vague English.
The Python Evaluation Rules document gives precise semantics for much of the Python language. It presents step-by-step rules for executing a Python program. Every skilled programmer uses such rules to reason about the effects of Python code. This document helps beginners to become experts more quickly. With this knowledge, a programmer finds it easier to write correct code, debug incorrect code, and read unfamiliar code.
The document applies to both Python 2 and Python 3. It does not cover every possible Python expression, but does cover the most frequently-used ones.
This document has been in use for 5 years, with great success. I recently moved to a new GitHub repository, where source code is available and you can submit bug reports or make pull requests.
If a programmer understands the language, then the programmer can understand what the program is doing and why it is producing the observed output. The programmer can determine a proper fix or devise meaningful experiments to better understand what values are being manipulated at run time.
Unfortunately, not all students are taught these simple, effective techniques. I have been horrified to see instructors (even at my own institution!) teach bad habits by telling students, "The only way to know what this program does is to run it." Many programming textbooks and websites are just as bad: they don't explain the programming model, or they do so in vague English.
The Python Evaluation Rules document gives precise semantics for much of the Python language. It presents step-by-step rules for executing a Python program. Every skilled programmer uses such rules to reason about the effects of Python code. This document helps beginners to become experts more quickly. With this knowledge, a programmer finds it easier to write correct code, debug incorrect code, and read unfamiliar code.
The document applies to both Python 2 and Python 3. It does not cover every possible Python expression, but does cover the most frequently-used ones.
This document has been in use for 5 years, with great success. I recently moved to a new GitHub repository, where source code is available and you can submit bug reports or make pull requests.
Thursday, August 11, 2016
Building robust distributed systems
Distributed systems are notoriously error-prone. It's hard enough for programmers to reason about multiple actions occurring on different nodes, but they also need to understand the messages that are sent among these nodes. (The problem becomes murkier yet in the presence of failures. A distributed system is designed to be faster and/or more reliable than a single-node system, but a distributed system contains more computers and connections, so it suffers component failures more frequently than the single-node system!)
I have been pursing several approaches to aid in the creation of distributed systems. Here are two of those projects.
To help programmers understand and debug distributed systems, my colleagues and I have created a visualization tool, ShiViz. Programmers typically debug distributed systems by examining their logs, but the logs are hard to understand. ShiViz creates a time-space diagram, a standard representation that programmers already use to represent the hosts and the ordering of messages between them. See the accompanying pictures of a conceptual time-space diagram and how ShiViz represents an actual execution. A time-space diagram shows when messages were sent and received, and thus it establishes causality: if event E1 occurred at node N before any effect of event E2 reached node N, then event E1 did not depend on E2. ShiViz works with existing logs, though it enhances them with causality information between events. ShiViz takes information that programmers would otherwise have to grep as text, and presents it in a form that programmers can explore, search, and understand. You can try ShiViz online, without having to install anything on your computer. Our article "Debugging Distributed Systems" appeared this month in Communications of the ACM. The article describes approaches to debugging distributed systems and shows when our visualization approach is a good choice.
To help programmers create distributed systems that are correct by construction, my colleagues and I have created Verdi, a framework for proving correctness of distributed systems. Verdi is a heavyweight approach built upon the Coq proof assistant: a programmer writes both source code and a proof of correctness for the source code, and thanks to the Curry-Howard isomorphism the program type-checks only if the proof is valid. This gives strong guarantees. While it is challenging to write such proofs for sequential code, it is much worse for distributed systems. Our system, Verdi, enables a programmer to write and prove a sequential program in Coq. Then Verdi transforms the program into a distributed system, and it transforms the proof into a proof of the distributed system. This approach, which we call "verified system transformers", abstracts away the difficulty of writing and proving a distributed system. Using Verdi, we created the first formally-verified implementation of the widely-used Raft consensus protocol. Our PLDI 2015 paper describes Verdi, and our CPP 2016 paper describes the proof in more detail. The CPP 2016 paper also explains the methodology that we developed while writing 50,000 lines of proof --- a methodology that significant eased the burden of using Coq and can be adopted by other researchers.
I have been pursing several approaches to aid in the creation of distributed systems. Here are two of those projects.
To help programmers understand and debug distributed systems, my colleagues and I have created a visualization tool, ShiViz. Programmers typically debug distributed systems by examining their logs, but the logs are hard to understand. ShiViz creates a time-space diagram, a standard representation that programmers already use to represent the hosts and the ordering of messages between them. See the accompanying pictures of a conceptual time-space diagram and how ShiViz represents an actual execution. A time-space diagram shows when messages were sent and received, and thus it establishes causality: if event E1 occurred at node N before any effect of event E2 reached node N, then event E1 did not depend on E2. ShiViz works with existing logs, though it enhances them with causality information between events. ShiViz takes information that programmers would otherwise have to grep as text, and presents it in a form that programmers can explore, search, and understand. You can try ShiViz online, without having to install anything on your computer. Our article "Debugging Distributed Systems" appeared this month in Communications of the ACM. The article describes approaches to debugging distributed systems and shows when our visualization approach is a good choice.
To help programmers create distributed systems that are correct by construction, my colleagues and I have created Verdi, a framework for proving correctness of distributed systems. Verdi is a heavyweight approach built upon the Coq proof assistant: a programmer writes both source code and a proof of correctness for the source code, and thanks to the Curry-Howard isomorphism the program type-checks only if the proof is valid. This gives strong guarantees. While it is challenging to write such proofs for sequential code, it is much worse for distributed systems. Our system, Verdi, enables a programmer to write and prove a sequential program in Coq. Then Verdi transforms the program into a distributed system, and it transforms the proof into a proof of the distributed system. This approach, which we call "verified system transformers", abstracts away the difficulty of writing and proving a distributed system. Using Verdi, we created the first formally-verified implementation of the widely-used Raft consensus protocol. Our PLDI 2015 paper describes Verdi, and our CPP 2016 paper describes the proof in more detail. The CPP 2016 paper also explains the methodology that we developed while writing 50,000 lines of proof --- a methodology that significant eased the burden of using Coq and can be adopted by other researchers.
Subscribe to:
Posts (Atom)