Benchmarking, parallel array reduction and interval arithmetic in Delite

During the past week Adam has been gathering performance measurements for the Acumen enclosure interpreter. He has been focusing on specific simulator parameters (e.g. the minimum ODE solver– and event localisation time steps) and the sensitivity of the end-time precision with respect to these. In order to make the measurements reproducible, Adam has adapted the benchmarking shell scripts that Kevin prepared previously. Further, Adam has been working on the assignments for the Heterogenous Parallel Programming course on Coursera, which this week involved implementing parallel array reduction in CUDA. Adam also prepared a project description for the project part of the Chalmers Scala course he attended in December. The project will aim to build an interval arithmetic library on top of the Delite framework, with a code generator for either OpenCL or CUDA. Initially, Adam plans to approach the implementation of the library by developing a sequential code generator for Scala.

How to restrict a grammar

In the past week Jan implemented a syntax checker for Acumen models intended to run with the enclosure interpreter. The checker validates that the model conforms to the subset of Acumen syntax used for the shallow embedding of a hybrid automaton. Jan has been working on a formalization of the Acumen subset in BNF form, but has found the formalism too limited to elegantly express certain aspects of the grammar. As an example consider the way events, i.e. transitions in the automaton, are expressed. This is done as follows: the underlying graph of the automaton is expressed by a single switch statement, with cases representing the hybrid modes. Events are specified by if statements, with an assignment to the mode variable indicating the target mode of the transition. Jan would like to constrain the grammar to require that there is precisely one assignment to the mode variable in each if statement, but has not found a way of doing this in plain BNF. As a quick fix he is considering adding this and similar constraints in natural language comments accompanying the grammar, but he is also looking at generalizations of BNF that would allow him to express this property within the grammar itself.

Localizing strategy continued

Last week Walid, Michal and Jan began working on a top-level strategy for the enclosure interpreter. Jan's original idea of reusing the constraint solver developed for the event detection and invariant intersection algorithms turned out not be suitable in its naive form. The problem with the idea is that it would not be able to ignore any events, and therefore not be able to localize the first event effectively. The solution is instead to use a subdivision-based approach that separately localizes the left and right endpoints of a segment of time that may contain the next event following. The segment is analyzed to determine if an event has with certainty been located and if continued sub-division is likely to localize the event further. Currently, an implementation is being finalized and integrated with the Acumen IDE. 

Scala course at Chalmers

During the past week Adam has attended an intensive Scala course at Chalmers, brilliantly presented by David Raymond Christiansen of ITU. The course introduced several aspects of advanced Scala programming, focusing on how its type system can be used with various approaches to embedding DSLs in Scala. Particular weight was given to Scala's implicit conversions mechanism, which e.g. makes it possible to emulate Haskell's type classes (with some additional flexibility) in Scala and can make interoperation with Java libraries smoother. The material of the course built up to the topic covered during the last day, a technique and framework called Lightweight Modular Staging (LMS). Adam found it easier to grasp after having understood the polymorphic DSL embedding technique, covered earlier in the week, of which LMS is an instance. In brief, this technique is based on defining the DSL as operations on an abstract data type. A program in the DSL is a nested call to these operations, and interpreters for the DSL are defined as implementations of the abstract operations which make up the program.

Progression of Zeno systems

During the past week Adam has been implementing a series of models developed by Walid, Jan and Adam, evaluating the enclosure semantics' performance on Zeno systems. An example of such a model is the following, inspired by a formulation of Zeno's paradox:

class Main(simulator)

  private

    d := 1; d' := -1;

    s := 1/2;

    mode := "q"; 

  end

  switch mode assume s <= abs(d)

    case "q"

      if s == d 

        s := s/2; 

        mode := "q" 

      end;

      d' = -1;

  end;

end

Adding a mode invariant (using the assume keyword) enables the interpreter to prune enclosures of impossible solutions, yielding a better overall enclosure. Though, at first glance, s <= d seems to be a suitable invariant for this system, this invariant does not hold after d crosses zero – changing this to s <= abs(d) ensures that the invariant holds for the entire simulation time. 

Adam will spend the coming week participating in a one-week Scala course given at Chalmers, learning about things such as implicit conversions, API design, polymorphic embedding of DSLs, scala-virtualized and LMS.

Towards a localizing strategy

Last week Jan integrated the new atomic step with the enclosure interpreter and started working on the top-level strategy. The idea has been to use the same constraint propagation technique employed to intersect enclosures with mode invariants and event guards during event handling. By composing event guards with the enclosures computed for the free variables in the guard and contracting the domain of the resulting predicate it should be possible to contract time segments around sub-segements where an event may occur. The advantage with this approach is that much of the necessary infrastructure is already in place, but a disadvantage is that it generally cannot show that an event has happened with certainty. 

Simpler atomic step

Last week Walid, Michal and Jan worked on a simplified version of the atomic step, i.e. the computation of an enclosure for a hybrid ODE-IVP over a fixed time segment. Jan implemented the specification and wrapped it in a function that makes it work as a drop-in replacement for the old atomic step, a.k.a. solve-VtE. Currently, the new atomic step produces a single constant enclosure for each variable, i.e. it cannot represent non-contiguous enclosures, such as those arising from discrete transitions in the simulation. This limitation can be lifted by changing the representation of the system state used by the new atomic step, from a single interval per variable and mode, to a set of intervals per variable and mode.