My favorites | Sign in
Project Home Wiki Issues Source
READ-ONLY: This project has been archived. For more information see this post.
Search
for
FAQ  
Answers to questions that are frequently asked, or would be if we had more users.
Featured
Updated Feb 1, 2012 by kevin.bi...@gmail.com

Introduction

This page contains a list of frequently asked questions. It doesn't really matter if they are actually frequently asked, as long as some future users are likely to appreciate the answer! If you have your own question to ask, please pose them to Kevin or Nels.

The Basics

How do I install Plural?

Please see the Installation wiki page.

I just installed Plural! What do I do now?

Well, that all kind of depends on what you want to do. But, assuming you don't just want to dive head-first into specification and verification, you might be interested in our regression suite, which contains a collection of working examples. This includes many of the examples from our various publications. This project can be found under PluralTestsAndExamples in the SVN directory. You should try checking out the project, and running Plural on some of the examples.

For more, check out the article GettingStarted on this wiki.

Which analyses should I actually run?

Once you have installed Plural, you will see a "Crystal" menu, and a number of analyses contained therein. The question is, which analyses should you care about and which can you ignore? Here is a brief explanation of each one. The basic analyses that you should use whenever you run Plural are highlighted.

  • FractionalAnalysis - This analysis is the main Plural analysis! It should always be selected if you are running Plural.
  • PluralAnnotationAnalysis - This analysis is really to improve the quality of error messages. It checks your annotations and ensures that they are well-formed. It's a good idea to select this analysis whenever you run Plural.
  • EffectChecker - Plural has a basic effect checker that can be used to improve its precision. If you don't know what an effect checker is, or if you aren't using the @NoEffect annotation, you probably can deselect this.
  • SyncOrSwim - Sync or Swim is a version of Plural that is sound even in the face of multiple concurrent threads. Generally you should not select this analysis unless your code is multi-threaded. If you intend to use Sync or Swim, deselect FractionalAnalysis or else you may get duplicate errors.
  • SyncChecker - A special annotation checker that should only be used if you are running Sync or Swim. This will give a little bit of extra feedback regarding the well-formedness of your annotations.
  • NIMBYChecker - NIMBY is the multi-threaded analysis that works for Java programs enhanced with atomic blocks. Unless you are using atomic blocks, you likely do not want to select this.
  • PolyInternalChecker - A much more advanced and unstable version of Plural that allows for polymorphic permissions. You likely do not want to select this.
  • LiveVariableAnalysis, ConstantAnalysis, any other analyses - These are basic static analyses that come with the Crystal framework and should be ignored when using Plural. They are unrelated. You probably want to uncheck them as well.

The Warnings

Plural's primary means of communication with the user is via Eclipse warning. This section discusses some of the most common warnings, and their meaning.

Plural says that an argument (or 'this') must be in a state or have a permission, but it is in no state at all or has no permission. Huh?

Are you getting a warning like the following?

argument this must be in state [next] but is in [] and argument this must have permissions [PURE(next) in [next]] but it has NOTHING line 287

This is probably the most important warning that Plural will issue, and certainly the most common. It usually occurs at method call sites or on method returns. Because it is so common, it is also a little hard to provide general advice on how to solve it, but here are some thoughts:

This warning basically means that you don't have as much permission as you need to satisfy the precondition of a method. Sometimes, as in this sample warning, it means you have no permission at all. Think about where the permission should be coming from. Often it's a constructor. Look at the constructor definition. Does it have a specification? Is any permission returned from the the constructor? If not, you must specify the constructor. Maybe the permission is actually supposed to come from the return value of a method. Look at the method. Has it been specified as returning any permission? If not, then you need to specify it.

Plural says that no context is available, possibly because of a previous error. Huh?

Are you getting a warning like the following?

[FractionalAnalysis]: No available context--usually due to a previous failure or error during packing/unpacking

This error is very generic, so you may get it in several situations. Usually it means one of two things:

  1. You are trying to access fields in a method, but the receiver permission does not include the flag, use=Use.FIELDS
  2. Earlier in the method, before the line where the error was reported, Plural tried to "pack" the receiver, which means, it tried to satisfy the invariants for one of the object states, and those invariants are requirements on field permissions. It could not do this, and therefore, it couldn't make any forward progress. To fix this error, try looking for program locations where the analysis would need to pack the receiver. Usually this is right before a method call. Make sure there is enough permission available to the fields for it to be able to pack to some state (usually any state will suffice).

Plural says that a dimension is already defined. What does that mean?

Are you getting a warning like the following?

[PluralAnnotationAnalysis]: Dimension already defined: current
Iterator.java /xxx/src/xxx/util/collections line 8 Crystal
Marker

This warning literally means that a state dimension is being defined more than once, and it can only be defined once. But there are a couple reasons why this could be happening. It's possible that you are defining a dimension twice in the same file. (Dimensions are generally introduced by using the @Refine and/or @States annotations.) But if you don't see these annotations twice in the same file, then it's likely that both a supertype and a subtype are declaring the same dimension. Look at the supertypes of the type where the warning is being issued. Make sure that each dimension is declared no more than once.

Plural says that I have inconsistent state space references. Plural says that a state is already defined. What does that mean?

Are you getting a warning like the following?

[PluralAnnotationAnalysis]: Inconsistent state space references: hasCurrent
not inside of current TupleManager.java

or

[PluralAnnotationAnalysis]: State already defined: available
TupleManager.java /xxx/src/xxx/data/tuple line 152 Crystal
Marker

Both of these errors indicate that something is going wrong in the definition of your state space hierarchy. Please see the response to the previous question for a resolution. You basically need to make sure that each dimension and state is only introduced once (using the @Refine and/or @States annotations). If a type has states or dimensions introduced by a super type, then it should not redefine them.

Plural complains about an implication not being satisfied even though that exact implication is in an invariant or a previous method post-condition. What can I do?

If you want to return from a method that declares an implication in its post-condition, call a method that has an implication in its pre-condition, or pack an object to a state whose invariant contains an implication you typically have to explicitly introduce that implication with an if statement, even if the required implication comes from another method call or a state invariant. For instance:

// alive's invariant: unique(f) * (canDo => f in enabled)
// YESICAN's invariant: canDo
private boolean canDo;
private MyType f;

@Pure @Perm(ensures = "result => YESICAN")
public boolean canDo() { return canDo; }

Plural will complain about the method not satisfying its post-condition even though it's rather obviously ok. What you need to do here is to help Plural establish the required implication:

@Pure @Perm(ensures = "result => YESICAN")
public boolean canDo() {
    if (canDo)
        return true;
    else
        return false;
}

What's the syntax for @Perm annotations and state invariants

You can require permissions, a typestate, or (in-) equality of variables and null, true, and false, and connect these atomic predicates with linear logic connectives , +, &, and ==>.

Notice we have never used + ourselves. When possible you want to use internal choice with a marker, e.g., instead of (this in A) + (this in B) you want to do something like:

@Perm(ensures = "(result == true ==> this in A) & (result == false ==> this in B)")

Although this particular pattern can have usually be abbreviated

@TrueIndicates("A") @FalseIndicates("B")

To get started on complex predicates we recommend you look at some examples in the code repository, such as the BlockingQueue. For your reference, the full Antlr grammar is here:

http://code.google.com/p/pluralism/source/browse/trunk/Plural/permission-parser/AccessPred.g

Are there Java features not supported by Plural?

There a number of unsupported Java constructs and features, including:

  • enhanced for loops
  • non-static and anonymous inner classes
  • local classes
  • auto-boxing and auto-unboxing
Note that concurrency is only considered with the relevant analyses turned on, see "basics" above.

Powered by Google Project Hosting