Current Trends in Computer Science (Conference)

I participated in a two-day conference organized by the Institute of Theoretical Computer Science in Prague entitled "Current Trends of Theoretical Computer Science" (STTI 2009). The presentations were invitation-only, which was mainly based on the criterion that the invitee had a publication at a well-established conference. The presentations were carried out in Czech and Slovak, which was a common source of amusement as few were used to that.

Talks

The number of talks was rather large so let me mention some representatives. The main talk was given by Viliam Geffert on finite state automate minimization. Minimization of standard DFAs is a well-known problem, this talk has addressed minimization modulo introducing finitely-many errors in the output of the result of the minimization. The motivation for such types of reduction is that if a certain device is running for an unbounded period of time, a finite number of errors at the beginning does not pose a problem.

Matus Mihalak presented a nice algorithmic problem in which a number of cops are guarding a certain region of a graph against a robber. Some complexity results were presented. For instance that the problem is NP-complete when the graph is a tree.

Another nice algorithmic problem was solved by Pavel Surynek: how to move a group of robots to desired destinations in a graph; with the additional objective to find minimal plans. This problem is motivated by traffic or warehouse organization. Pavel has targeted a special case when the graph is 2-connected. For intuition, Lloyd's 15 puzzle is a special case of this problem.

A problem from the bio-informatics was presented by Brona Brejová. Given a Hidden Markov Model (HMM) and a chain of transitions, one is to find the most probable sequence of states in the model that would correspond to the sequence of transitions. The classical algorithm solving the problem uses memory proportional to the length of the transition-sequence and number of states in the HMM. This is too much for the examples coming up in bio-informatics and thus Brona and her coauthors devised an online algorithm discarding unneeded memory.

Several talks were on complexity classifications. Stanislav Živný presented some of his results on so-called submodular polynomials. These are pseudo-boolean polynomials satisfying an additional constraint called submodularity. Minimization of these polynomials can be done in cubic time for quadratic polynomials. Stanislav has been investigating for which polynomials can minimization be translated into minimization of quadratic ones.

Jiri Srba gave an overview of recent complexity results for Visibly pushdown automata. Those are such pushdown automata where each operation must always push/pop a fixed number of symbols from the stack. These automata are interesting for program verification as equivalence is decidable (in program analysis the stack models the callstack). One of the mentioned results of Jiri was that deciding bisimulation for visibly pushdown automata is EXPTIME-complete.

Eva Jelínková has presented a problem from the graph realm. Eva has investigated the complexity of deciding whether a clustered graph can be drawn nicely in a plane. A clustered graph is graph in which nodes may be contained in clusters; clusters are either disjoint or one is a subset of another. By nicely I mean that the clusters can be drawn as closed curves that do not intersect.

Rastislav Královic presented a problem from the networking domain. Rastislav has investigated how strong of an opponent can we have when the game is that we need to send a message in a network and the opponent is allowed to discard certain number of messages. One of the presented results was that a message can still be delivered even if the opponent can discard all but one message in each step.

Problem Section

An interesting part of the conference was the Problem Section, where whoever wanted presented a small (open) problem. I have presented a problem that I've bumped into recently and Radu wrote up here (I was a bit surprised that I haven't got an answer or pointer (yet)).

Martin Klazar has presented a so-called Skolem's problem which was is it decidable that a recurrent sequence hits a 0?

Libor Barto has presented a hard-core question, what is the minimal tree for which H-coloring is NP-complete?

Summary

All in all, I would like to say that it was a nice experience. All participants came neither for fame nor for money and still the talks were given in an excellent quality. I'm glad that I went as I enjoyed the overall spirit of the conference and not only I learned about the result of my countrymen but about theoretical computer science in general.

P.S. apologies to those whose names are not spelled properly but my patience is quite limited when it comes to diacritical problems :)

P.P.S. Mr. Nesetril, the program chair, told me that it is not correct that anybody could have participated in the Problem Section as he filtered the topics beforehand.

Program verifiers are complex

I've recently found out that epitome is not only a Romanian word but also an English one. The discovery deserves a blog post.

Programs instruct (virtual) machines what to do. Programs tell type-checkers what to check. Programs can also tell program verifiers what to check. A (static) program verifier is a little like a type-checker on steroids. Unlike type-checkers, they tend to be complex beasts. ACL2, Jahob, and Spec#, all tame the complexity in different ways.

The approach in Jahob is code reuse. The developers chose to rely heavily on the work of others and innovated mainly in the area of "putting things together".

Spec# divides and conquers, much like Microsoft does in general. They broke down the process of verification into multiple simpler phases and built probably the best engineered program verifier.

The old ACL2 encodes complexity in data rather than code. More specifically Moore (yes, the same guy who did the string matching algorithm) notes that there is no need for verification condition generation if you simply tell a prover the operational semantics of the language you are processing.

It's funny how the oldest tool has the slickest approach (and, probably, the smallest number of developers). Here are some references:

• Full functional verification of linked data structures
• Boogie: A Modular Reusable Verifier for Object-Oriented Programs
• Inductive assertions and operational semantics

Data Structures in Imperative Languages

So in the past few weeks I have realized I don't really know how to write data structures in Java or in any other imperative language for that matter.

The issue is that once one wants follow certain patterns like visitors or immutable classes, lot of code has to be written by hand in a tedious and repetitive fashion.

The reason is that these design decisions affect all the data structures in a similar way: a visitor pattern requires an accept method for each class; equality, hash code, cloning have the same properties over all classes (such as deep cloning); etc.

Code generation does seem like a good path to follow here.

Thanks to a colleague who is an avid UML modeler I had the opportunity to work with classes generated via the Eclipse Modeling Framework (EMF).

So how did I like it? Not too much. There's almost no control over the code being generated as the template is well embedded in the innards of the framework.

No equals method, no hashCode method, no make methods (which create a class from the given attributes). All have to be written by hand - get me out of here!

Hence I went and looked for other technologies.

A colleague of mine Radu developed a light-weight tool for the purpose in question. The class diagram is specified in a custom language similar to grammar description languages. For instance:

BinaryOperator :> Implies, Iff;

tells us that the classes Implies and Iff extend the class BinaryOperator. The code is generated using templates, which are language-ignorant and may access properties of the classes using special keywords.

For instance, \ClassName is expanded to the name of currently processed class and \BaseName to the name of the base class. This enables us to write templates like this:

public class \ClassName extends \BaseName { ....

More details about Radu's tool can be found in this article.

Radu's approach is nice, concise, and more flexible than EMF. The problem is, however, the template language. Very soon I have discovered that there are properties of the classes that are hard to access. Moreover, it's not quite clear how one extends the generated classes with custom code.

Even though tempted to extend the existing tool with constructs of my desire, I decided to look for other existing approaches based on code generation using templates.

Surprisingly enough, little did I find. The most promising is described in a tutorial using the velocity tool. The tutorial can be found here.

The template language is richer, it supports if statements, variables, and other goodies. Theinclude construct, I believe, could be used to extend classes with custom code.

The language is a bit awkward at times, this could probably be overcome by defining some velocity variables. It seems that one would have to write support for navigating the structures describing the class diagrams one wants to support.

All in all, I have a nagging, ominous feeling that I'm missing something. Is it not the case that pretty much every object orient program needs data structures? Isn't there like million papers on UML and/or code generation?

Could someone please point me to a decent tool that would let me generate data structure code using templates driven by class diagrams?

Matthew Parkinson verifies Java. Very brief and inaccurate version.

Here are some slides. (His last slide in the first set is ``do David's exercises.'' Obviously, you'll need to know what those were in order to solve them. David's exercises were ``do John's exercises.'' Happy solving!). Here's a summary of the lectures:

• Q: How to model abstraction? A: Use uninterpreted functions.
• Q: How to use separation logic to verify Java programs? A: Use intuitionistic separation logic because it plays well with garbage collection.
• Q: How to deal with inheritance? A: Attach to each method a static spec and a dynamic spec.
• Q: How to reason about concurrency? A: Use a mix of separation logic and rely/guarantee reasoning; we'll call it deny/guarantee.

Do you want more? OK, here's one example. The Visitor pattern is used often by people who write compilers. When you write a.f(b, c) you call function f with three parameters. The first one, a is special in two ways: (1) it will be known by the special name this in the body in of the function and its dynamic type is used to decide which of the functions named f will be called; in general, more than one function f may be called by the same statement depending on the value of a. The Visitor pattern is a work-around not having multiple dynamic dispatch aka multimethods. Or, depending where you come from, you might see it as a work-around not having pattern matching. The main tool used by this pattern is (single) dynamic dispatch, so it will also illustrate how to annotate programs that use this feature of Java.

interface Ast { Ast accept(Visitor v); }
class Constant implements Ast {
  int value;
  @Override Ast accept(Visitor v) { return v.visit(this); }
}
class Plus implements Ast {
  Ast left, right;
  @Override Ast accept(Visitor v) { return v.visit(this); }
}

interface Visitor {
  Ast visit(Constant n);
  Ast visit(Plus n);
}

Given this boilerplate we can do something `useful' to the AST.

class ZeroRemover implements Visitor {
  @Override Ast visit(Constant n) { return n.value == 0? null : n; }
  @Override Ast visit(Plus n) {
    n.left = n.left.accept(this);
    n.right = n.right.accept(this);
    if (n.left != null && n.right != null) return n;
    return n.left != null? n.left : n.right;
  }
}

If you are unfamiliar with the Visitor pattern you can spend a few minutes starring at the code above. Or you could continue reading and notice how sprinkling annotations actually helps to understand the code. So, how do we annotate the accept method? If the visitor and the AST node are OK (for some definition of OK depending on the visitor and on the node, respectively), then some value will be returned (for some definition of some, depending on the particular visitor. OK, so we'll just say what we just said.

interface Ast {
  Ast accept(Visitor v)
    requires this.OK(t) ** v.OK(o)
    ensures v.Result(result, this, t, o);
}

``Whooooaa, stop! What's the funny **, and what are t and o? You said you'll write exactly what you said!'' Uhm, the stars are just the separating conjunction; we use two because one is taken by multiplication. The t and o is just stuff, uninterpreted for now if you want. We're just saying that the Result may depend on the state of the node and on the state of the visitor. Feel better? Yes? OK, then let's move on, it's late. I'll skip some specs so we can move quickly to the next interesting bit. How do we say what ZeroRemover is supposed to do? We just provide a definition for the Result predicate, which was uninterpreted (or `abstract') until now.

class ZeroRemover implements Visitor {
  spec
    Result(r, a, t, o) = r == rz(t);
    plus(Constant(0), x) = x;
    plus(x, Constant(0)) = x;
    plus(x, y) = Plus(x, y);
    rz(Plus(x, y)) = plus(rz(x), rz(y));
    rz(x) = x;

  @Override Ast visit(Constant n) { return n.value == 0? null : n; }
  @Override Ast visit(Plus n) {
    n.left = n.left.accept(this);
    n.right = n.right.accept(this);
    if (n.left != null && n.right != null) return n;
    return n.left != null? n.left : n.right;
  }
}

Let's recap: In the specs you write a Haskell program that does the same thing but is shorter and (perhaps) slower and also some bridges between Haskell (aka math) and your program. As a result you can run a tool to tell you if your efficient(?) Java program does the same thing as the Haskell one.

Now, can you fill in the specs that I skipped? If not, then please do ask in the comments what information you feel you are missing.

Separation logic

A good way to learn separation logic is to read Reynold’s introductory lecture notes. This is a little bit like saying that a good way to learn programming is to read Knuth’s books. If you are the type of person that likes using iPhones and searching with Google you might need a bit more to wet your appetite.

Separation logic was designed to allow local reasoning. ‘Local’ is a generalization of ‘modular’. You can say ‘local’ when you have some sort of distance and you can say “a is close to b but far from c.” We reason locally when all the stuff that we need to keep in our head at one time is ‘close’. ‘Modular’ is simply ‘local’ specialized with program text distance. The typical distance people have in mind when they talk separation logic is “the number of pointer indirections I need to do to get from location x to location y.” When you think about a linked list you tend to ignore other linked lists that are at distance ∞. Good, so the central concept of separation logic is locality; or separation, depending on how you look at it.

A logic is a very simple language with very precise semantics. To describe the logic (that is, the one most people know) you need to introduce operators and describe what they mean (for example, p ∧ q evaluates to ⊤ when both p and q evaluate to ⊤); in other words, you introduce a piece of syntax and then you give its semantics. Thinking in terms of semantics is not always efficient. Sometimes you need to get in the symbol crunching mood. That’s why you’d typically present rules for manipulating symbols that are sound (for example, p ∧ (q ∨ r) can be replaced by (p ∧ q) ∨ (p ∧ r)).

There are three pieces of syntax that are new in separation logic: the separating conjunction p ⋆ q, the points-to operator x → v, the separating implication aka the magic wand p −⋆ q, and emp. The semantics are described in terms of a somewhat more complicated model. Now we have not only booleans plus some abstract domain. Still, the model will be familiar to any programmer. We have addresses, values, a stack (inappropriately named ‘store’ by the old-timer Reynolds), and a heap. (BTW, there’s nothing wrong with ‘store’ per se. It’s just that most programmers prefer the ambiguous terms ‘stack’ and ‘heap’.) So,

• p ⋆ q holds in a heap that can be split in a part where p holds and a part where q holds,
• x → v holds in a heap that has exactly one cell whose address is x and whose content is v,
• p −⋆ q holds in a heap that can be extended with a heap where p holds to get a heap where q holds,
• emp holds when the heap is empty.

Once we introduce these new operators we also get new laws, such as:

• p₁ ⇒ p₂ and q₁ ⇒ q₂ can be replaced by p₁ ⋆ q₁ ⇒ p₂ ⋆ q₂
• p₁ ⋆ p₂ ⇒ p₃ can be replaced by p₁ ⇒ (p₂ −⋆ p₃)

In fact there are classes of assertions for which extra rules can be used.

• pure assertions are those that don’t say anything about the heap so they can be pulled out of the new operators; for example (p ∧ q) ⋆ r can be replaced by p ∧ (q ⋆ r) if p is pure,
• strictly exact assertions are those that uniquely identify the heap,
• precise assertions are those that identify a unique subheap
• intuitionistic assertions are those that hold for any extended heap
• supported assertions are those for which there is a least subheap on which they hold

Now we can annotate programs with descriptions of the state at various intermediate points. If we also have rules on how the state is changed by simple commands we can then derive formal proofs of programs, meaning that the annotations can be shown to agree with the program by pure ‘symbol crunching’, something even a computer should be able to do. People who write such programs have a knack for funny names: Space Invader and Smallfoot. Well, perhaps not all people who write such tools. There is also the Unnamed and Unreleased tool from Matthew Parkinson that handles Java code. Edit: Matthew pointed out that the tool has a name: jStar. (Please write a comment if another tool should be mentioned here.)

The interesting algorithms proved correct (in the sense explained above) using separation logic are Schorr–Waite and Michael’s stack. (Please write a comment if another algorithm should be mentioned here.)

Let me briefly present these two algorithms.

The Schorr –Waite algorithm is used to reduce memory usage during garbage collection. For our purposes ‘garbage collection’ simply means that we want to mark all reachable nodes from a given root. The simple solution is to do a DFS. A simple implementation would use a stack of pointers that may grow in the worst case to be linear in the number of nodes in the graph. The trick Schorr and Waite use is to use the link fields in the graph to store the backpointers.

Michael’s stack is lock-free and works in the presence of memory reclamation. You want to implement push(stack, node) and pop(stack), where stack is a pointer identifying the stack. These functions will be used from multiple threads and the only synchronization primitive you are allowed to use is the compare-and-swap statement. To push a node you would probably try to read stack->next, set node->next := stack->next, if stack->next == what I read then set stack->next := node. The last operation is the compare-and-swap: “If the first element of the stack is still what it was when we looked the first time then make node the new first element.” The problem with this is that “the same first element” doesn’t necessarily mean “the next pointer of the first element is the same.” No one is supposed to change the next pointer apart from push and pop, but it may very well be that the node is freed, a ‘new’ allocated node happens to be the same area in memory and then there is nothing holding back the change of the next field. That is, unless you use an array of stuff that shouldn’t be touched, as in the solution given by Michael.

That’s it for now. Oh, and sorry if you were under the impression that I’m trying to ‘wet your appetite’. I was merely trying to draw a child’s sketch of separation logic.