In order to reason about control-oriented models such as state machines, automata, and imperative programming models in a compositional manner, the Coroutine Model of Computation has been developed as a general denotation formalism for such control-oriented models. In the Coroutine Model of Computation, Coroutine models can be defined to characterize control-oriented behavior either as an entire model of a system or as a control-oriented component in a heterogeneous system. In the latter case, a Coroutine model can be used to represent modal behavior, complex exception handling mechanisms, or the integration of imperative components into dataflow models and synchronous models. This heterogeneous composition is possible and straightforward to reason about because this Model of Computation has a simple interface-oriented dynamic semantics.

The Coroutine Model of Computation consists of atomic elements called Continuation Actors, which like the Actors of Modular Actor Interfaces have inputs, outputs, and state spaces, along with functions to produce outputs and update internal states. The model of an Actor is extended to a Continuation Actor adding to the interface a function that can make control decisions directing the containing model to suspend the process in the Continuation actor, terminate execution, or abort execution of the Continuation Actor proceeding to some other process. Coroutine Models are then defined as networks of these Continuation Actors in which control flow traverses the network directed by control decisions each Continuation Actor makes along a control path. The composition of Continuation Actors in a Coroutine Model form itself a Continuation Actor, allowing Coroutine Models to be composed hierarchically.

A further novel feature of this Model of Computation is that meaning is given to non-strict Continuation Actors, which can make partial control decisions given partial information about inputs. Correspondingly, a non-strict dynamic semantics is defined for Coroutine Models containing these non-strict Continuation Actors. When individual Continuation Actors allow for multiple control decisions, the traversal of their network in a Coroutine Model forms a tree of control paths, and a denotational semantics is given for combining the information along each possible path to produce both partial outputs and partial ultimate control decisions for the whole model. The semantics devised for this non-strict behavior for a Coroutine Model is monotonic when the contained Continuation Actors are monotonic, hence such Coroutine Models can be used meaningfully in the context of a fixed-point semantics like that of Synchronous Reactive models. This non-strict semantics also allows Coroutine Models to be synchronously composed as is done in Constructive Esterel and SyncCharts.

In addition to the formalism being developed for Coroutine models, a preliminary implementation has been written in Ptolemy II, and further development of this model will follow along several research directions. One of these will be to use the formal language and practical implementation of the model to unify several other models of computation such as SyncCharts, Modal Models, Control Flow Graphs, and exception handling mechanisms. Practical case-studies will also be developed to demonstrate the power and breadth of this formalism. Finally, the possibility has been explored to use Coroutine Models as a means of modeling the execution strategy of other models. This work has been published in a paper coroutines.

In order to study the semantics of Models of Computation implemented in ptolemyII, with an particular interest in the meaning of their composition in heterogeneous models, Modular Actor Interfaces was developed to give a clear mathematical description of these models. In the language of Modular Actor Interfaces, an Actor is given a mathematical model consisting of its input, output, and state types, its initial state, and four interface functions:

1. Fire:
   This function maps states and input values to output values, and is used to produce output for the actor remaining in its current state.
2. Postfire:
   This function maps states and input values to new state values, and is used to update the state of the actor.
3. Deadline:
   This function maps states and input values to times, and is used to determine the latest time at which the Actor can be fired.
4. Timeupdate:
   This function maps states, input values, and time durations to new state values, and is used to update the state of an Actor as a function of the passage of time.

In this language, a model consists of a set of Actors, each having the above elements, connected together by their ports into an Actor Graph, as well as to ports for the model. Given a particular Director, representing a Model of Computation, the model becomes itself an Actor. The Director describes how to build the spaces and interface functions of the model from those of the contained Actors and from the Actor Graph. As such, the Director acts as an Actor combinator parameterized by the structure of the Actor Graph.

This details regarding this formal treatment of ptolemyII Models of Computation is given in the article modularSem, which will be published in Mathematical Structures in Computer Science. In order to work with this formalism directly, a kernel of ptolemyII functionality called PTuring was developed in Haskell. Future plans for this research involve understanding better the relationships between models of computation described in this formalism and what the consequences are of heterogeneous compositions of various Models of Computation.

Models developed in the ptolemyII platform are expressed primarily in the diagrammatic language of ported networks of Actors. While there are many ways to mathematically represent these networks as abstract graphs or hypergraphs, there is little syntax-direction and modularity to this kind of a syntax. Expressing compositional properties can only involve the single type of composition characterized by joining graphs, which can change the topology of the joined graphs radically.

An Alternative syntax for Actor graphs is one that expresses structure modularly in terms of combinators that are used to algebraically construct representations of Actor graphs as syntactic terms. Such a syntax often involves three basic combinator elements:

1. Parallel Composition
   Two substructures are combined without connections such that the set of inputs and outputs of the composition are simply the combination of the inputs and outputs of both combinatands.
2. Sequential Composition
   Two substructures are combined by connecting the outputs of one to the inputs of the other.
3. Feedback Composition
   A feedback loop is formed over a substructure, usually from some particular output to some particular input.

In addition to these combinators, there are a set of primitive elements used to permute, split, join, or terminate connections, as well as an identity of some sort. There are many examples of such a syntax that appear to have been independently developed. Some of these are:

1. Stefanescu's flownomials: Flownomials
2. Milner's ccs
3. Pentrose's diagLA: Diagrammatic methods in Linear Algebra
4. The faust: Faust programming language
5. Megacz's genArrows: Generalized Arrows in Haskell

Of these approaches, the first, flownomials appears to be a very developed and general framework for understanding the role that these combinator syntaxes play in the development of semantics. For this reason, I am beginning to look into using flownomials as a basis for developing a theoretical framework for a combinator syntax of Ptolemy models upon which semantics can be reasoned about in a proof-theoretic fashion. Stefanescu and Broy in broynomials, for instance, use flownomials as representations of dataflow models, giving algebraic identities modeled by the given dataflow semantics. This constitutes a means by which to create an axiomized theory of dataflow models. A similar approach can be taken, I think, with the diverse collection of models of computation developed in Ptolemy.

I have done some preliminary work in this area, mostly during 2010, during which I developed code in Ptolemy to transform models into such a combinator-based syntactic representation. I am planning on continuing to pursue this line of investigation in 2013, focusing particularly on the mathematics of flownomials, which I had been unaware of when I started the work but clearly represents the best basis for this research.

During the Spring of 2012, I began to research the mathematical structure of Evaluation Mechanisms as a class project. I am planning on continuing this work with a focus on how to understand it in the context of Ptolemy Models of Computation. The motivation behind this research was the paper kowalski by Kowalski, which suggested that algorithms could be divided into two separable components that determined what value to compute and how to compute it. While the former is captured well by declarative specification in Logic and Functional languages, the latter is a less obvious control-oriented specification that in practice often takes the form of annotations. However, in hudak Hudak proposes that partially-ordered multisets be used as a mathematical representation of evaluation schemes in functional languages, which seems to be a good basis for a mathematical method of reasoning about evaluation. Even more recently work has been done by [refs] to develop Evaluation Strategies in Haskell as stand-alone specifications of evaluation that can be applied modularly to programs. My class project investigated these lines of development and drew some connections to operational semantics.

I intend to continue pursuing this research to the end of understanding how an understanding of evaluation mechanisms in Ptolemy Models of Computation can bridge the gap between the denotational specification established in Modular Actor Interfaces and abstract specifications of execution. This can be viewed as a search for a new way to look at scheduling.

The PRET project aims at the development of architectures and programming methods that constitute a software platform with Precision Timed (PRET) execution behavior. More specifically, PRET architectures for microprocessors have fine-grained worst-case execution times for individual instructions. PRET platforms have predictable worst-case timing characteristics, and thus timing can become a core part of their semantics. Given the power to make fine-grain guarantees about time, the timing characteristics necessary in real-time and safety-critical systems can be established on the level of semantic correctness rather than empirical verification.

During the Fall of 2012, I worked with zimmer on a project to design FlexPRET, a PRET architecture with flexible thread scheduling. This work elaborated on the PTARM design of Isaac Liu developed in his thesis ptarm. The FlexPRET processor implements most of the RISC-V ISA and has fixed execution time for each instruction depending only on the number of active threads and the previously executed instruction. It has a scratchpad memory rather than a cache, and has no branch prediction. The design choices for this processor were aimed at maximizing throughput as much as possible without introducing hard to predict mechanisms that introduce complex and hidden forms of state into execution. Currently, the design has a 5 stage thread-interleaved pipeline, separate instruction and data scratchpads, supports integer operations excluding division, and has a software controlled interleaving schedule.