Shared Resources

We are proposing an approach to the development of concurrent systems based on a sharp distinction between active (processes, clients) and passive (interactions, resources) entities. This admittedly simplistic view of concurrency will help us, however, in achieving some of the aforementioned goals. For example, synchronization and communication primitives (often language-dependent) will appear only inside the implementation of the shared resources, not in the process code. This separation will facilitate to work on the verification of the processes on relatively standard grounds. On the other hand, the implementation of the shared resources will be ensured to be correct by construction, using template-based code generation schemes both for shared memory and message-passing schemes, rather than verified a posteriori. This simplifies portability. Also, the method is supported by a graphical notation intended to be reminiscent of UML class and collaboration diagrams.

Name Brief Description Graphic Spec TLA JML Java Ada Erlang KeY
Airport Traffic Control Tower The local airport has only two runaways for landing and take off.
Semaphore* Semaphores are a technique for coordinating or synchronizing activities in which multiple processes compete for the same resources.
Bounded Semaphore* Semaphores are a technique for coordinating or synchronizing activities in which multiple processes compete for the same resources. This variant allows up to n processes waiting
Bounded Buffer A variation of a producer-consumer problem using a buffer of only ONE element in which Producers add new items to the buffer whilst consumers get and remove a given number of items.
Bounded buffer with Selection Likewise a bounded buffer. Producer processes add new elements (natural numbers in this example) to the buffer, and consumer processes remove elements from it. Items are read from the external world and written back to it.
Bounded Multibuffer A variation of a producer-consumer problem using a bounded buffer in which Producers add new items to the buffer whilst consumers get and remove a given number of items.
Memory Manager A memory request returns n consecutive free slots from address i. In order to simplify the solution, when a process dealloc memory it knows from which address and the number of slots to be set free.
Readers-Writers* Many threads must access the same shared memory at one time, some reading and some writing, with the natural constraint that no process may access the share for reading or writing while another process is in the act of writing to it.
Parking Parking slot in a building .
The Recycling Plant Steel is recovered from unsorted domestic waste with automatically controlled cranes equipped with electromagnets: cranes collect steel and deposit it in a container until the container is (nearly) full.
Printer Spooler The printers at the Green Itch reprographics center are environment-aware and can safely estimate how many pages that can be printed before a toner cartridge replacement is needed. This functionality is intended to avoid partially printing a job, saving operator time, and optimizing the usage of toner cartridges. A single printer server gathers printing requests from users and communicates with the printers. Users send jobs to the printers through clients.
Observer - Event Manager The Observer design pattern (Chapter 5 of the book Design Patterns by Gamma, Helm, Johnson and Vlissides) is one of the most applied design schemes in programming (reactive systems, interfaces user, etc.). Its operation is based upon a set of events issued by a component (such as I/O operation, updates on a ADT), which observers subscribe. When one of these events occurs, all observers subscribed are reported to act accordingly. We have adapted the pattern so we'll have processes that generates and emit events and processes that subscribe to a subset of them. The formers are listening until one event that are subscribed is issued, reacting accordingly.
Shipping Warehouse A warehouse complex where autonomous robots move around fulfilling shipping orders. The weight of the robots, in any given warehouse, should never exceed a certain maximum weight.

* Parameterless shared resources

Generic placeholder image

SRViz

Visualization of a shared resource implementation behaviour using Babel Priority Monitors - TBA

View details »

Generic placeholder image

Razor

Translator from annotated Java code to TLA - TBA

View details »

Generic placeholder image

Shared Resource Erlang Testing

A framework/toolbox for testing a class of safety-critical concurrent systems implemented using shared resource specifications.

View details »