This page presents a collection of Java programs that have been specified and/or verified using Plural/NIMBY. Full details of the tool can be found in several locations, but the best starting point is the Plural project page on Google Code. This includes the full source for both Plural (single-threaded protocol verification) and NIMBY (concurrent protocol verification), as well as links to various papers. More importantly, that page is easier to update and is connected to the SVN repository, so it is much more likely to be up-to-date!
These are the programs described in the OOPSLA '08 paper, Verifying Correct Usage of Atomic Blocks and Typestate by N. Beckman, K. Bierhoff, and J. Aldrich. These programs are part of the Plural/NIMBY test suite, and therefore should verify with the current version of NIMBY at all times.
| Example Name | Source | Notes |
| Chat | Chat.java | The Chat example is used as a running example throughout the paper. The main difference here is that we use Java annotation syntax as required by the NIMBY tool. |
| JGroups JChannel |
JChannel.java CausalDemo.java | These two files represent the specification of the JChannel class, an abstraction of a network connection from the JGroups project, and the implementation of one of the demos that is provided with JGroups. This demo, CausalDemo, makes use of the the JChannel protocol. |
| Request Processor | RequestProcessor.java | Request Processor is a simple, toy program that was specified and verified to illustrate that our approach could handle object invariants of mutable, thread-shared objects. |
| Reservation Manager | ReservationManager.java | Reservation manager was the original program that was going to be used as a running example throughout the paper. It is still somewhat interesting, but, frankly, not as realistic as the Chat program. |
The following are a list of other programs that I have specified and/or verified with Plural/NIMBY as part of my research.
| Example Name | Source | Notes |
| Blocking Queue |
Blocking_queue.java OneReaderOneWriter.java |
This example is the full example that was presented in the OOPSLA 2008 talk on NIMBY. It's a thread-shared blocking queue. Note that the blocking queue class was written by Allen I. Holub, and is used with permission. Thanks! The verification of both the implementation side and the client work. The client is in the OneReaderOneWriter file. |
| Thread Shared and Back | ThreadSharedAndBack.java | In this example, we take an object that is thread local, share it between two threads, and then reconstruct the unique, thread local permission. This is a sort of litmis test for many concurrent analyses. Note that we are using the parameter "capture" mechanism of PLURAL in order to ensure that the fraction that comes back from the other thread is the same. We haven't completely verified the implementation of the join method, but the fact that the join method requires a full permission and does not return it should ensure that no permissions could be duplicated. |
| ConsList |
ConsList.java Lambda.java Lambda2.java |
A functional-style cons list with a very simple protocol: EMPTY or NONEMPTY. There are also some interesting protocols in the two iterator methods, although they have already been specified by Kevin in earlier work. |