Title: A Type System For Safe SN Resource Allocation

Authors: Michael Ocean and Assaf Kfoury and Azer Bestavros

Abstract: 

snBench is a platform on which novice users compose and deploy
distributed sense and respond programs for simultaneous execution on a
shared infrastructure. It is a natural imperative that we have the
ability to (1) verify the safety/correctness of newly submitted tasks
and (2) derive the resource requirements for these tasks such that
allocation may occur. Other works provide static analysis techniques
(i.e., type systems) to bound the size of data in order to establish
an upper bound on a program's required computational resources (i.e.,
storage and CPU time). We recognize a significant shortcoming in these
approaches: The upper-bound approach breaks down in many scenarios in
which data has other relationships that must be tracked. This is
especially true when images are considered a first class data type, as
some image manipulation functions may require a particular minimum or
maximum resolution to operate correctly. In fact, the results here
have benefit beyond the application to image data, and may be extended
to other data types that require tracking multiple dimensions (e.g.,
image "quality", video frame-rate or aspect ratio, and audio sampling
rate). In this technical report we present our work to provide a sized
type system for our functional-style Domain Specic Language (DSL)
called Sensor Task Execution Plan, or STEP. Our sized type system
provides an estimate of computational resource requirements as well as
resource requirements derived from implicit constraints in the static
analysis of STEP instances. We can use use these constraints to
statically verify program safety, guide resource allocation, or
enforce run-time checks that ensure the run-time behavior adheres to
the static analysis.  We present the syntax and semantics of our
functional language, our type system that builds costs and
resource/data constraints, and (through both formalism and specic
details of our implementation) provide concrete examples of how the
constraints and sizing information are used in practice.