The acceptance of Ruby in the scientific community lags a bit behind, partly because it is missing a good library for linear algebra and vector programming. It has a matrix class in its standard library, but its execution tends to be rather slow. Only a couple of actual scientific computing libraries like NumPy for Python exist for Ruby. In this paper we introduce a new library called Bohrium.rb. Bohrium.rb acts as a front end for the Bohrium framework, which generates and runs JIT-compiled OpenMP/OpenCL kernels. It currently supports Python/NumPy and C++, however as it is built of processes communicating hierarchically to each other, we can replace the front ends with new ones. This new Ruby front end is described with examples and is then compared to the standard library and an already established Ruby library Numo/Narray, where Bohrium.rb seems to be faster for still larger matrix calculations. This is also the trend we have seen in similar areas with Bohrium, being faster once its overhead has been amortized.
Concurrency is beginning to be accepted as a core knowledge area in the undergraduate CS curriculum – no longer isolated, for example, as a support mechanism in a module on operating systems or reserved as an advanced discipline for later study. Formal verification of system properties remains considered an advanced and difficult subject area, requiring significant mathematical knowledge and generally restricted to smaller systems employing sequential logic only. Our experience, from over 30 years of teaching concurrency and formal methods, is that when both are presented together, there is a happy symbiosis providing strong mutual support that transforms both disciplines from advanced and hard to basic and simple. Of course, the model of concurrency and formal methods presented must be simple, powerful and consistent with each other … and, of course, we are talking about process orientation and process algebra.
By utilizing Synchronous Message Exchange (SME) for hardware design, we see that going from a hardware schematic to an implementation becomes a much shorter process. This in turn shifts the focus to the architectural details of the implementation. This is shown by constructing an implementation of the Transputer in SME. This implementation has been made in less than 800 lines of code within the timeframe of ~4 months, where the majority of the time spent has been on the Transputer architecture. The resulting implementation is suboptimal compared to similar projects. However, since no optimizations have been made, reaching a more reasonable resource consumption and clockrate should be attainable within a few months.
We show how to apply the technique of data refinement from the field of Formal Methods to test or verify scientific parallel programs by generalizing the concept of abstraction functions to distributed data structures. This work is motivated by experience of developing computationally-intensive finance models to support the London Insurance Market and the application of test-driven development to achieve correctness by design.
The growth from terabytes of 3D imaging data and soon approaching petabytes from material analysis has left the scientists involved with a set of challenges. In particular, the ability to efficiently analyze an ever growing collection of material tomography scans. The MUMMERING research project aims to solve this by providing ability to submit workflows to automate the process of analyzing the collected data. We explore and present our initial design thoughts in this endeavor. This includes a proposal to utilize the IDMC system developed at UCPH to provide an efficient method in terms of scheduling and execution of workflows. Beyond this mere exploration of thoughts about a potential solution for the MUMMERING project, this paper will also we introduce our initial work in providing ubiquitous access to the produced datasets. The aim here is to provide a simple API for loading/storing datasets during an image analysis, by providing this universal data access library (i.e. mig_utils). With this we hope to help the non computer scientists involved in defining imaging analysis programs that easily either can executed locally during the experimentation phase or subsequently scheduled by a workflow scheduler.
CSP is an algebra for reasoning about concurrent systems of processes. Being able to do so has become a necessity for computer scientists. Having to think about abstractions like mutexes and threads in practice can be cumbersome, complex, and erroneous. Ruby as a programming language has been described as fun to program in. It is however missing a CSP framework that it can call its own. Emit, which is presented in this paper, tries to mitigate this by providing such a CSP framework. As a CSP framework, Emit makes it easy to think about processes, channels, and communication. It is not yet feature complete, however comparing it to its nearest peer, PyCSP, shows good performance for the COMMSTIME benchmark, where Emit is 100 times faster.
The XC programming language is designed to make runnable multitask programs for XMOS' xCore multicore microcontrollers, spread on tiles and cores. This presentation addresses only a few aspects of XC. What is a combinable and what is a distributable task, syntactically and semantically, but also resource wise and geographically on the chip? The xCore compiler handles the lowering of interfaces onto statically and dynamically allocated channel resources. The microcode and built-in scheduler also reflect them. Of the rather limited amount of resources, one must make it with 32 chanends per tile, with seemingly loose coupling between the XC code and the final number of chanends. Fiddling around, rather overwhelmed, with [[combine]], [[combinable]], [[distribute]], [[distributable]] and [[distributed(..)]] plus par and on reveals a lot of how unchanged functionality spreads differently over cores or across tiles. Thus the same functional code may require anything from, like, six to zero chanends! The goal of this fringe presentation is to trigger interest, not provide answers. Or rather, only those answers that the author might presently have acquired by surrendering to this can of reserved words and observe what might possibly happen. Like, there must be an electric motor inside, because the sound of it is so pleasant.
While CSP is traditionally taught as an algebra, with a focus on definitions and proofs, it may also be presented as a style of programming, that is process-oriented programming. For the last decade University of Copenhagen (UCPH) has been teaching CSP as a mix of the two, including both the formal aspects and process-oriented programming. This paper summarized the work that has been made to make process-oriented programming relevant to students, through programming assignments where process orientation is clearly simpler than an equivalent solution in imperative programming style.
Not only can (and should) concurrency be introduced early in the undergraduate CS curriculum – but mechanisms for its formal analysis and verification can be presented that are intuitive, effective and easy to learn and apply. Further, this can be done without requiring students to be trained in the underlying formal mathematics. Instead, we stand on the shoulders of giants who have engineered the necessary mathematics into the concurrency models we use (CSP, π-calculus), the programming languages/libraries (occam-π, JCSP, Process-J) that let us design and build efficient executable systems within these models, and the model checker (FDR3) that lets us explore and verify those systems. All we require from our students are a love of the subject, a flair for programming and some time and effort. This talk presents some experience over the past ten years that lets us make these claims.
Anyone who knows process-oriented programming immediately acknowledges the claim that process orientation is well suited for games programming. As it turns out, this is easier acknowledged than done since there are no game programming frameworks that support an external threading library, but rather all insist on managing threads within the game framework. This fringe introduces an idea, as of yet without any implementation, to integrate visual effects directly within PyCSP.
Given the prior knowledge of implementing SME (Synchronous Message Exchange) onto hardware, describing small hardware becomes very simple. This is shown by constructing a Pong inspired game in SME, in approximately a week, which runs on an FPGA (Field-Programmable Gate Array). The game uses the VGA port as output and the buttons on the board as input, and as such runs purely on the FPGA. The game consists of two larger parts: the VGA controller and the game logic, with the VGA controller being the most problematic part to
In this paper, we introduce a new channel to the Bohrium runtime system that supports lossy compression of data. This channel makes it possible for a local user to offload calculation and data heavy processing to a remote server and still be able to visualize the data over a modest network connection. The new lossy channel supports a fixed frame rate mode where the user can specify a desired frame rate that the lossy channel will maintain. In order to maintain a frame rate, the lossy channel will dynamically adjust the quality setting of the lossy encoding.
This paper presents a modelling approach and software tool support for automatically deriving reusable Go components from CSP prototypes that preserves compatibility with existing CSP verification tools. Using the example of a concurrent component that generates prime numbers, the paper demonstrates how to model and verify a parameterised concurrent component in machine-readable CSP, and presents the software tool's automatically-derived implementation of this model as a reusable Go component.
The Go programming language defines simple I/O interfaces that any data type may implement. In this paper we introduce a Go package that allows arbitrary implementations of these interfaces to be composed into RAID-like redundant (and/or) high-performance striped arrays. The package also allows spares to be added for fail-over functionality. The package is focused on providing a highly available write setting that tolerates multiple failures but can always receive data as long as a single redundant path exists. This is achieved by allowing reads to become unavailable in the presence of failures that cannot be solved while the array is operating.
This Fringe presentation will continue the comparison of the two approaches from our first talk (“Formal Verification for IoT”) in rigorous mathematical detail. We introduce the mathematical concept of a Covering-with-Boundary (CwB), prove the equivalence of cycle-counted occam on a Transputer with this path diagram, and proceed to prove cases that avoid both divergence and effective divergence by finite restrictions. Due to static characteristics of occam-and-Transputer-based “Ground Truth,” we are also able to prove Hardware-Software Equivalence, and reach IoT conclusions that extend to non-digital payloads.
Cluster computers are seen as expensive, space consuming, high energy platforms hidden away in universities and tech companies. Having your own cluster computer to explore parallelism ideas was not realistic for the majority of people. With the release of the Raspberry Pi things changed, and now it is possible to build a five node machine powered by USB that you can hold in your hand for as little as £120. This talk will describe how such a machine can be built with very little technical knowledge, and then provide an example of setting up MPI on the machine to allow simple distributed parallel applications to be explored. The system is not fast, and communicates via a shared USB 2.0 connection, but the principles of distributed parallelism can be explored. An example system will be available for demonstration purposes.
WACOMSAS (WAsteful COMmunication SAtellite System) uses the Transterpreter to demonstrate a finite, static occam-based design for a ground station that communicates with at most four passing satellites at a time. There may be an indefinite number of satellites, each of which may never return. The satellites are not coded in occam, and external channels with mobile channel ends are used to communicate with them according to a switchboard analogy applicable both to hardware and software interfaces. The occam solution is compared to similar implementations in Go and Python/PyCSP, and environment that simulates satelites with Arduinos is set up and used for eksperiments.
Given the presentation of the Pong inspired game at last years conference, we bring you another, more complex arcade game. This time we have partially implemented Space Invaders running on an FPGA (Field-Programmable Gate Array), which renders the screen directly to the VGA output of the board. Furthermore, to improve the usability of the game, we have connected the wires of an NES controller directly to the board, in order to control the game.
Performance is important when creating large experiments or simulations. However it would be preferable not to lose programmer productivity. A lot of effort has already been put into creating fast libraries for for example linear algebra based computations (BLAS and LAPACK). In this paper, we show that utilizing these libraries in a DSL made for productivity will solve both problems. This is done via automatic code generation and can be extended to other languages, libraries, and features.
