Tagging; Transition Kompilation Option

In this lesson we add the semantics of variable increment. In doing so, we learn how to tag syntactic constructs and rules and then use such tags to instruct the kompile tool to generate the desired language model that is amenable for exhaustive analysis.

The variable increment rule is self-explanatory:

rule <k> ++X => I +Int 1 ...</k>
     <env>... X |-> N ...</env>
     <store>... N |-> (I => I +Int 1) ...</store>

We can now run programs like our div.imp program introduced in Lesson 1. Do it.

The addition of increment makes the evaluation of expressions have side effects. That, in combination with the non-determinism allowed by the strictness attributes in how expression constructs evaluate their arguments, makes expressions in particular and programs in general have non-deterministic behaviors. One possible execution of the div.imp program assigns 1 to y's location, for example, but this program manifests several other behaviors, too.

To see all the (final-state) behaviors that a program can have, you can call the krun tool with the option --search. For example:

krun div.imp --search

Oops, we see only one solution, the same as when we ran it without search.

Here is what happens. krun can only explore as much of the transition system associated to a program as kompile allowed the generated language model to yield. Since most of the K users are interested in language models that execute efficiently, that is, in faster interpreters for the defined languages, by default kompile optimizes the generated language model for execution. In particular, it inserts no backtracking markers, which krun uses when called with the --search option in order to systematically generate the entire transition system associated to a program. This is why krun showed us only one solution when run with the --search option on div.imp.

We next explain how to tell kompile what kind of language model we are interested in for analysis purposes. When you experiment with non-determinism in a language semantics, you should keep it in mind that the --transition option of kompile allows you to configure what counts as a transition in your language model. We here only discuss transitions due to the non-deterministic evaluation strategies of language constructs, but we will see in future lectures (see Lesson 6 of IMP++, where we add concurrency) that we can also have transitions due to non-deterministic applications of rewrite rules.

If you want to explore the entire behavior space due to non-deterministic evaluation strategies, then you should include all the language constructs in the --transition option. This may sound like the obvious thing to always do, but as soon as you do it you soon realize that it is way too much in practice when you deal with large languages or programs. There are simply too many program behaviors to consider, and krun will likely hang on you or crush. For example, a small ten-statement program where each statement uses one strict expression construct already has 1000+ behaviors for krun to explore! Driven by practical needs of its users, the K tool therefore allows you to finely tune the generated language models using the --transition option.

To state which constructs are to be considered to generate transitions in the generated language model, and for other reasons, too, the K tool allows you to tag any production and any rule. You can do this the same way we tagged rules with the structural keyword in earlier tutorials: put the tag in brackets. You can associate multiple tags to the same construct or rule, and more than one construct or rule can have the same tag. As an example, let us tag the division construct with division, the lookup rule with lookup and the increment rule with increment. The tags of the rules are not needed in this lesson, we do it only to demonstrate that rules can also be tagged.

The least intrusive way to enforce our current language to explore the entire space of behaviors due to the strictness of division is to kompile it with the following option:

kompile imp.k --transition "division"

It is interesting to note that the lookup and increment rules are the only two rules which can trigger non-deterministic behaviors for division, because no other rule but these two can ever apply while a division operation is heated. Previous versions of K allowed you to also specify which rules could trigger non-deterministic behaviors of operator evaluation strategies, but that option was rarely used and is not available anymore.

Note that it is highly non-trivial to say precisely whether a strict language construct may yield non-deterministic behaviors. For example, division's strictness would yield no non-determinism if the language had no side effects. It is even harder to say so for a particular program. Consequently, our K implementation makes no attempt to automatically detect which operations should be tagged as transitions. Instead, it provides the functionality to let you decide it.

Now the command

krun div.imp --search

shows us all five behaviors of this program. Interestingly, one of the five behaviors yields a division by zero!

The --transition option can be quite useful when you experiment with your language designs or when you formally analyze programs for certain kinds of errors. Please let us know if you ever need more finer-grained control over the non-determinism of your language models.

Before we conclude this lesson, we'd like to let you know one trick, which you will hopefully not overuse: you can tag elements in your K definition with kompile option names, and those elements will be automatically included in their corresponding options. For example, if you tag the division production with transition then the command

kompile imp

is completely equivalent to the previous kompile command.

Please use this default behavior with caution, or even better, try to avoid using it! You may be tempted to add the transition tag to lots of elements and then forget about them; your language models will then be increasingly slower when you execute them and you may wonder why ... This convention is typically convenient when you want to quickly experiment with non-determinism and do not want to bother inventing tag names and calling kompile with options.

In the next lesson we add input/output to our language and learn how to generate a model of it which behaves like an interactive interpreter!

Go to Lesson 4, IMP++: Semantic Lists; Input/Output Streaming.

MOVIE (out of date) [06'56"]