1. Tiago Cogumbreiro Avatar Tiago Cogumbreiro
  2. Untitled project
  3. armus

Wiki

Clone wiki

armus / HOWTO Verify OpenMP

View History

Quick development plan

  1. Represent OpenMP blocking operations as resource-dependency edges.
  2. Interface OpenMP with Java: 2.2. Choose a platform agnostic API (Redis) 2.3. Implement a verification strategy in Armus that uses Redis 2.4. Check the overhead of the new backend against NPB. 2.5. Extend Armus-X10 backend to support multiple places. 2.6. Implement a C bindings for Armus (armus-c).
  3. Manually instrument OpenMP
  4. Automatically instrument OpenMP

Introduction

To be able to check OpenMP with Armus, we need to know how to represent each blocking operation with resource-depedency edges. With this knowledge, we must instrument any blocking primitive and communicate the generated resource-dependencies to Armus. Furthermore, we must periodically enquire Armus for deadlocked states.

Now, we need to be able to answer the following questions:

  1. How to represent a blocking operation with resource-dependency edges?
  2. How to instrument OpenMP?
  3. How to interface Armus and OpenMP?

How to represent a blocking operation with resource-dependency edges?

OpenMP has two basic synchronisation mechanisms: barriers and locks. In JArmus, we already check barriers and locks, so this code can be used as a starting point. Locks were added because of the project of OpenMP verification.

References:

How to instrument OpenMP?

While we do not have an instrumentation library, we can manually the OpenMP programs. There are some deadlocked examples listed in the references below. But, before we start, we need to know how to interface OpenMP and Armus (i.e., the following topic).

References:

How to interface Armus and OpenMP?

In short, we want to turn the Armus API into a service, so that OpenMP can access it. The idea is to expose classes VerificationStrategy and TaskHandle with a platform agnostic API.

What about JNI? The problem of JNI is the source of instability that it may generate (i.e., any crash will bring the whole thing down), plus going for a platform agnostic API is a step towards to support the distributed setting.

Requirements of the Armus API

  • Each OpenMP thread calls a invokes TaskHandle.setBlock and TaskHandle.clearBlocked and Armus should provide the implementation for these calls.
  • Method calls setBlock and clearBlocked are very frequent and cannot block
  • Only the last call of setBlock and clearBlock matters.

Update: The outcome of this work is summarised in interface ArmusDAO. The C API should be similar.

In summary, if we see OpenMP as the writer and Armus as the reader:

  • Writes have to be really fast, ideally made asynchronously. Reliability is not crucial.
  • Only the last write of a given OpenMP thread is important (one write overwrites the previous write)

With this in mind, key/value systems seem to be more appropriate for this type of communication. Redis seems to be the most interesting.

References:

Updated