Wednesday, February 27, 2013

Event tree analysis in hybrid system simulation

Last week Walid, Michal, Jan and Adam finished a revised specification for an event detection and handling procedure for hybrid systems based on explicit tracking of event sequences. The sequences are gathered into a structure encoded as a tree, analogous to the event trees used in to analyze causal relations between events in hazard analysis. Along with an event, each node in the tree also encodes an approximation of the states that are reachable from the states approximated in the preceding node. The information encoded in the event tree makes it possible for the procedure to sometimes detect that all reachable states have been accounted for, even when the event tree contains an infinite branch.  

Monday, February 25, 2013


WiffWaff (by Adam Duracz and Yingfu Zeng) is the Acumen player that won the first tournament of 3D Ping Pong project as part of the Halmstad CPS course in 2012. Terminator (by Jonas Jonson and Alexey Taktarov) won second place in first tournament in 2013. But local rankings can be deceiving! Terminator is a new bread of players that is much more sophisticated than anything developed in 2012.


The result is clear from this game, where WiffWaff is on the left (red), and Terminator is on the right (black). Note the small balls that show Terminators predictions about bounce position and bat impact position. When a player turns into a yellow cube, it means it ran out of energy. Terminator is the first player that is able to successful complete the 40 second game against itself, returning every ball, and within the energy budget.

Congratulations to the new Alexey and Jonas!

OpenCL matrix multiplication

During the past week Adam has been focusing on course work, including the Embedded Parallel Computing course for which an OpenCL implementation of matrix multiplication was developed. While OpenCL shares many similarities with CUDA, using the bare API does require writing a lot of boilerplate code. For example, configuring a kernel function for execution on a GPU device requires explicitly connecting to the device, fetching its ID, creating a compute context and a command queue to which the kernel call will be enqueued. Before this can be done, each kernel function parameter needs to be set by an individual function call! Compared to this, in CUDA, it suffices to annotate the kernel function call with an execution configuration, which for simple programs can amount to a one-liner:

kernel_name <<< blocksInGrid, threadsInBlock >>> (x,y,z)


The rest of the application, including host as well as kernel code, is more similar, and OpenCL does provide some convenience functions which are not present in CUDA, for example get_global_id(x), which does the same thing as CUDA's ubiquitous blockIdx.x * blockDim.x + threadIdx.x incantation (calculating a thread's global identifier). The additional effort of an OpenCL implementation does however translate to portability, meaning that code written for one GPU has a good chance of running on another GPU or even on some other platforms, though without any guarantees with respect to performance. Also, recent developments in libraries and bindings such as SimpleOpenCL or PyOpenCL could give many of the benefits of CUDA (perhaps more) while retaining most of OpenCL's portability.

Monday, February 18, 2013

IDE PhD winter conference

During the past week Adam attended the IDE PhD winter conference, where he presented his work on generator-driven testing of XSL transformations. Aside from getting feedback on his work, the conference was an opportunity to interact with research students from across Halmstad University and included presentations on topics such as Ambient Assisted Living, infrared detectors based on carbon nanotubes, extensions of the LLVM compiler infrastructure and SLAM-based robot navigation. Adam also worked on defining research questions for his PhD and found this book chapter to be helpful when formulating them.

Monday, February 11, 2013

Jawad Weekly Update

Jawad had created the first simulation case for the active driver assistance systems longitudinal function called Collision Imminent Braking. The simulation case describes the testing vehicle approaching from behind towards the reference stationary object (car/pedestrian). The simplest possible mathematical models were modeled using new version of Acumen and Acumen 3d e.g. the car was represented by a point mass without friction; the straight road was represented by a fixed rectangular box; the sensor was represented by the single variable which calculate the distance between testing vehicle and stationary vehicle; one dimensional force was applied in x-axis direction while all forces in remaining five dimensions (two translations and three rotations) were neglected; The deceleration of testing vehicle was modeled by applying braking force in negative x-axis direction; the activation of function was modeled when distance sensor detects the critical distance (< = 3m) between testing vehicle and the reference vehicle. Jawad had also participated and presented these simulations at CISER 2013 internal conference and industrial workshop. Jawad will continue to simulate the ADAS functions as part of NG-Test project where he will be exploring the possibilities of including Acumen as tool in Automotive V model for cyber physical system design.

First steps in OpenCL and a bisecting root finder

During the past week Adam has been focusing on the Embedded Parallel Computing course, which introduced vector machines and the related GPU architectures. As part of this course, Adam is re-implementing some of the laboratory exercises which were part of the Heterogeneous Parallel Computing Coursera course, but now in OpenCL instead of CUDA. Kevin helped Adam in modularising the vector addition host code as a C++ class, making it easier to re-use in subsequent implementations. Work on the interval arithmetic library for the Chalmers Scala course is also moving forward. With the help of Jan he wrapped a bisection algorithm around the basic Interval Newton algorithm to complete the validated root finding algorithm, all implemented on top of the library.

Sunday, February 10, 2013

Loading obj files and 3D text syntax modification

Last week, Yingfu and Kevin added a new feature of Acumen3D that is loading the .OBJ file.
One needs to declare the type of the object to be "OBJ" and specify the path at the end.
The following example loads the R2D2 robot model:

class Main(simulator)
  private
    _3D :=["OBJ",[0,0,0],1,[0,0,1],[3.14/2,0,0],"robot/r2d2.obj"];
  end
    _3D = ["OBJ",[0,0,0],1,[0,0,1],[3.14/2,0,0],"robot/r2d2.obj"]
end

Currently, all the related files(.obj, .mtl and textures) should be located under the _3D folder in the main directory.
The syntax of 3D text was also changed, the type has to be "Text" and the content should be specified at the end. 

Regression tests for Acumen's enclosure interpreter

Last week Adam and Jan cleaned up the generator-driven property based tests for Acumen and introduced a simple regression test for the enclosure interpreter. The test checks that the enclosures produced for each model in a specified directory are identical with the expected enclosures computed using a baseline version of the interpreter. The addition of the regression tests will help maintain functionality intact during refactorings of the enclosure interpreter.

Friday, February 1, 2013

Basic Interval Newton, parallel scan, caches and pipelining

During the past week Adam has been focusing on course work for the three courses he is attending. This included finishing the implementation of parallel scan for the Heterogeneous Parallel Computing Coursera course, reading about caches and pipelining for the Embedded Parallel Computing course at HH, and pushing the implementation of the interval arithmetic library forward for the Chalmers Scala course. In the latter, work has been focusing on a basic implementation of Interval Netwon's method for finding the zeros of real functions has been implemented (univariate case), backed by a Scala code generator. Once Interval Newton has been implemented using the library, the major remaining part of this work is the development of a code generator for either CUDA or OpenCL.

Formal specification of Acumen's enclosure interpreter

Over the past weeks Jan, Walid and Michal have been writing down a formal specification of the algorithm underlying the Acumen enclosure interpreter. The specification includes a number of theorems formalizing the most important properties of the algorithm, such as definedness, safety and convergence. The main difficulty with formulating these theorems has been the lack of universally accepted definition for the trajectory for a hybrid system after its first Zeno point. The pragmatic approach taken was to use a commonly accepted definition for trajectories up the the first Zeno point and to restrict the theorems to such trajectories. For evolutions beyond the first Zeno point the output of the algorithm is taken to define the behavior of the system. The specification work has exposed a number of opportunities for vast performance improvements which will be the focus of Jan's coming work.