multicoredafnyformal-verification

How to create a constant reference to an object in Dafny


I am trying to create a model of a multicore system in Dafny. Usually, in multicore systems (and in the system I'm modelling), there is an idle task -- a placeholder task that is run when a core doesn't find any other work to do. This task will only be created when the system starts, its fields are incremented (because it is run, but its running has no real meaning), but the reference itself never changes.

I am struggling to define such a task in Dafny. My attempts:

class Task{
   blah blah blah...
}

class MultiCoreSystem{

   static const idleTask : Task // ERROR: static non-ghost const field 'idleTask' of type 'Task' (which does not have a default compiled value) must give a defining value
   
   static const idleTask : Task := new Task(0) // ERROR: Calls with side-effects such as constructors are not allowed in expressions.

   static var idleTask : Task // ERROR: a field cannot be declared 'static'
}

And I tried doing the same declarations in Task too, to no avail.

I could also just use nullable references, so if a core finds that the current task is null it just spins, but it's much cleaner if there is an idleTask.


Solution

  • Dafny is closer to a functional programming language to be honest. It has classes but you can't use them in quite the same way. All side effects and heap initializations must be done within a method. A constant in Dafny is a module level feature and it can only be immutable data and not a heap object (aka class).

    module MultiCoreSystem {
        class Task {
            var id: int
            constructor(taskId: int)
                ensures this.id == taskId;
            {
                this.id := taskId;
            }
        
        }
    
        method RunMultiCoreSystem() {
            var idleTask : Task := new Task(0);
        }
    }