Compiler-plugin for protocol verification

Compiler
#1

Hi, I am making a compiler-plugin for Scala to check that classes which have an assigned protocol follow that protocol (it is meant to implement session type theory from pi-calculus).

I am basing it on this Java tool: Mungo and StMungo for Java

With the tool, a user could add a protocol file to a class/object, which would look like a statemachine with methods of that class causing transitions.
e.g. for a file we might want to make sure that it is opened before it is read and then that it is always closed.
The tool would then check how that class is used and that it does not violate its protocol.

To add a file I was thinking of using an annotation with the name of the protocol file. Then the file could look like this:

typestate fileProtocol{
State0 = {
    open(): Unit => State1
}
State1 = {
    read(): Unit => State1,
    close(): Unit => end
}
}

(Typestate is just another word for protocol)

I am planning to make this as a plain compiler-plugin (with Antlr to translate the protocol file).

Basically, since I don’t really use Scala much, I was wondering what you all think of this implementation idea. Is the representation of the protocol intuitive? Are there better tools I should use? Any ressources would also be appreciated.

#3

Hi @Alice. Is the protocol specification format fixed? Or it’s something you are designing? In the latter case, my intuition is that reusing Scala’s parser and type checker might make your life easier. You could define your protocols using Scala syntax, which is rather flexible and can easily be enriched via annotations. In the protocol specifications, you could thus refer to the described classes using actual type-checked references to these classes, in a way that tools such as IDEs understand (so that, for instance, one can control-click on them, or even rename them). Does that make sense?

#4

Hi, I can define the protocol however I want so that is an intriguing possibility.
I am having difficulty picturing what you mean though, could you give me an example?

#5

The key concept here is that Scala is a pretty good language for building DSLs (domain-specific languages). That can be leveraged to the point of absolute abuse, as demonstrated here – more practically, though, you can build a lot of “languages” that are actually just carefully-designed Scala functions. The concept is discussed in various places: for example, here’s a chapter of a book on the subject, and here’s an article about it.

1 Like
#6

btw, maybe the session types approach can be interesting for you. What I recall now:

#7

Sounds like a great project! It indeed sounds like session types. State machines are very intuitive, although of course a bit verbose (see below).

Wrt. defining this as a Scala DSL (using Scala’s own syntax), using Scala’s support for defining internal DSLs, I also think I would try that first. It is not problem free though since one would have to define a sub-language of Scala, which the compiler plugin can recognize! in order to perform the check for conformance between a class and its specification. This is the eternal battle between external DSLs which are easy to analyze and internal DSLs which are easy to execute.

I myself developed an internal Scala DSL for event monitoring:

https://github.com/havelund/daut

The idea behind this DSL is to verify the execution!! of some system against a specification (in contrast to verifying the code against a specification). Since it is the execution one can also refer to data transferred in method calls, which would be a challenge in a static approach (making verification hard).
Some techniques in this DSL may be useful for defining a typestate DSL. E.g. the above spec could be written shorter by inlining State1 as in something like:

typestate fileProtocol {
  always {
      case open() =>  hot {
           case read() => stay,
           case close() => end
      }
  }
}
#8

Hi @LPTK,
Thanks for the answer! I did go ahead and make a DSL but I’m struggling to get referencing to the classes. Can you point me to some ressource about this? And is it alos possible to reference methods?

#9

Thanks for the answers and the advice on DSLs!

I made one which looks like this at the moment:

in ("State0")
when ("walk(String)") goto "State3"
when ("comeAlive()") goto "State0"

in ("State3")
when ("die(): Boolean") goto "State3" at "True" or "State0" at "False"

end

I couldn’t seem to get rid of the parenthesis after the “in” and “when” commands for some reason. I also am not sure how to link the methods to the ones actually defined in the class or if this is even possible.

#10

Hi, I guess it depends what implementation strategy you choose. Do you still want to make it a compiler plugin? A macro-based library? Something which uses runtime reflection (you could require users to run the specification so it performs its checks at runtime)?
All are viable implementation strategies. I’d recommend trying to use macros first, though the Scala 2 experimental macro implementation is very rough and has a steep learning curve. If you want to use Dotty, you could use Dotty’s TASTy-reflect-based inspection instead, which would probably be much cleaner and less buggy (but less stable, since the interface is still being refined).

In terms of the DSL, one interface you could achieve would look like:

object State0 extends State[TheClass] {
  when (_.walk(???)) goto State3
  when (_.comeAlive()) goto State0
}
object State3 extends State[TheClass] {
  when (_.die()) goto State3  at true or State0 at false
}

Or, another possibility:

object TheClassSpec extends Spec[TheClass] {
  lazy val State0 = State {
    when (_.walk(???)) goto State3
    when (_.comeAlive()) goto State0
  }
  lazy val State3 = State {
    when (_.die()) goto State3  at true or State0 at false
  }
}

Whichever implementation you choose, you should be able to retrieve the method symbols identifying each method, based on lambdas like _.walk(???).

There are really a lot of ways of doing things. Yet another one would be to just use annotations in the class itself, and check these annotations separately.

#11

Thanks for the info.

Is the DSL only going to work with runtime checks then? Or can it also permit compile time checking?

#12

Compile-time checking can be done in many ways: by running your tool as part of a macro, a compiler plugin, a build tool plugin (see: SBT plugins), as a custom rule in the build tool, or even asking users to run the tool manually in the test suites of their apps :^)

#13

Thanks, I’ll look into these things!

#14

With respect to related work, there is this: https://alcestes.github.io/effpi/

2 Likes