How can we summarize the behavior of composite reactors? #1307
Replies: 7 comments 5 replies
-
Very interesting ideas! Our current interface information provides some of this, e.g. whether a partial function is delayed or not, but not the distinction between a function and partial function, which is often important (e.g., to be able to infer periodic sources downstream from clocks). What @lsk567 is working on, where he parses the reaction code and analyzes simple patterns, has the potential to provide a conservative over approximation that will infer these types automatically. |
Beta Was this translation helpful? Give feedback.
-
I know you wrote that this is not about syntax, but since it is not a very prominent feature, I want to make sure that people are ware of the generics syntax that we already have. You can actually write |
Beta Was this translation helpful? Give feedback.
-
I think another discussion worth having is what we even mean by higher level functions in LF. If all we want to do is provide library reactors that implement a certain pattern while allowing users to specify the precise functionality, then I think all that we would need are function pointers (or lambda functions). In fact, this already works in the C++ target. See the following example:
It prints:
|
Beta Was this translation helpful? Give feedback.
-
I tried to formalize some of these ideas in this document. Unfortunately the PDF is too long for me to ask anyone to read it in detail, and I have had difficulty purging it of false statements. However, I'll share it now because a month has passed since I promised @lsk567 that I would write it, and because the rate at which I have been finding counterexamples has gone down. The document is also somewhat related to conversations I had recently with @erlingrj. Related: #1464 (for addition of logical times), #805 (for another reason to place restrictions on what I refer to as smears) UPDATE: It seems like we might choose elementwise addition of logical times, in which case most of the gnarly, distracting details in the PDF will disappear. (This is being discussed in #1464.) (**EDIT 6/3/23: We agreed many months ago not to use elementwise addition. We are still using the noncommutative addition.) EDIT: When I wrote "strongly connected component" on page 18, I actually meant "complete subgraph." EDIT (6/23/23): A quote from Kahn (1974):
|
Beta Was this translation helpful? Give feedback.
-
My GitHub notification settings were misconfigured earlier, which made me unaware of all of the interesting discussions here for the past few months... Overall, this seems to be a very interesting proposal. The proposed type annotations remind me of two closely related areas of research: This seems to be exactly what you are doing but for Ptolemy II and with specifications written in interface automata. You can definitely get some inspiration from here. Assume-guarantee (AG) contracts are essentially specifications that describe the behaviors of components in a system. Each contract is a pair of an assumption (on the environment) and a guarantee (on the component). In plain English, a contract is essentially saying "if the environment can provide these conditions specified in the assumption, then this component can guarantee these behaviors: ..." AG contracts are usually written in some formal logic. It turns out that if one organizes specifications in the form of contracts, there exist handy operations that enable compositional reasoning by composing or decomposing contracts. @YuTaiwan and I worked on a course project together two years ago on this topic. We tried to generate contracts for reactor components and perform compositional verification. Your type system could behave like a contract. For example, a reactor of type Not sure if the above is in line with what you have in mind. Hopefully you find it helpful. :-) |
Beta Was this translation helpful? Give feedback.
-
Relationship with tokens/smart pointersOne of the claims made here was that it is desirable and possibly feasible to extract information about the logical time intervals between events on certain elements of programs, such as ports. Here is another use case for such a thing: if implemented, it would lead to an alternative to the token/smart pointer mechanism with different tradeoffs. Related: #1526 MotivationImagine a If the video frame is completely processed in a single timestep, then the rest of the program can re-use the memory on the output port of the However, if a downstream reactor wishes to use the video frame at a later tag, then it must schedule the video frame into the future. Use cases for scheduling such a large object into the future include
If I understand, the C target supports such use cases by requiring the video frame to be wrapped in a token, and incrementing a reference count on that token when the video frame is scheduled into the future. Reference counting is a time-tested solution that works well in practice for many important applications. However, I am under the impression that a reference-counting-based approach is inherently based on dynamic memory allocation. Dynamic memory allocation is a symptom of not having statically checked how much memory we will use. It also tends to make performance less consistent and less predictable than is possible without dynamic memory allocation. So, it is possible to imagine wanting a "more static" approach that has more predictable run-time behavior, at the cost of requiring more information at compile time. IdeaThe form of lifetime annotations that has been popularized by Rust lets programmers annotate their programs with guarantees that some reference will be valid (i.e., it will not point to freed memory) for as long as some other reference will be valid. If we can extract information about the logical time intervals between activity in certain subprograms -- for instance, if we can reduce the then we can guarantee that a certain reference will be valid for any period that is strictly less than 100 logical milliseconds (right-)plus one microstep. Example 1Suppose that a reactor that is downstream of Then the In this case this version of the Example 2Suppose that a reactor Then the In this case this version of the Example 3Suppose that a reactor Then the Therefore, this case is the same as example 1. Further developing the ideaIt is possible to ask whether it makes sense to consider giving lifetimes of state variables, it is possible to ask whether it should be permitted for a reactor to mutate one of its outputs without setting it, and it is possible to ask when downstream reactors are allowed to modify their inputs (I understand that this last question has been addressed with our mutable inputs mechanism, but the answer could be different in a slightly different context). However, I have not considered these questions yet because it should first be determined whether any notion of lifetimes in LF is worth investigating in the first place. |
Beta Was this translation helpful? Give feedback.
-
It is a great idea to consider the connection between our notion of logical time and the lifetime of objects (I would be very curious to see how a Rust like language would work if it has a logical lifetime concept built in). However, I have some concerns with respect to the proposal laid out here. Edward already pointed out that tokens are not inherently connected to dynamic memory allocation. The same is true for smart pointers in general. First and foremost, smart pointers allow to model ownership of data. Knowing about ownership, it becomes possible to also free memory that is not owned but anyone (kind of like garbage collection). This, however, is only a secondary concern. The STL smart pointers use dynamic memory allocation by default, but they are not limited to that. In fact, you can pass a raw pointer to any object (independent of if and how it was allocated) to It is not quite clear to me what the motivation is here. Are you concerned about performance in general? Or is this more about memory constrained platforms and time predictability? I have experimented with using memory pools to speed up the allocation of "tokens" in the C++ target, but to my surprise this performed much worse than the default fully dynamic strategy. After reading up a bit on this topic, I found that malloc/free is heavily optimized and its hard to beat this with other strategies. malloc is only slow and unpredictable if memory tends to get heavily fragmented. However, in applications like the one you describe, the allocation pattern is very regular. Even without any lifetime annotations, an malloc/free based implementation is very likely to give you the desired behavior. If you always free a block of size I am also concerned with respect to composability. I think it is generally a bad idea to make the behavior of one component dependent on the components that are connected to it. Maybe a better angle would be to think about this in terms of guarantees. A reactor Now we tell our users not use raw pointers. And with the approach that I laid out in the above paragraph it would be difficult to verify that no one violates the contract. However, I think the same would be true with the lifetime approach. How would you guarantee that no one uses a reference to some data after its lifetime exceeded? To me, Peter's description sounds very much like sending raw pointers in disguise and there is not much of a guarantee one can give in C. Generally, I am under the impression that this is trying to solve a problem that is better solved by domain experts. Engineers working with a certain platform know best how to allocate memory on this platform. Also predictability is a very application specific concern. So I find it would be better to give users the tools to build their custom solution, instead of trying to have a LF solution that then likely would not fit all the use cases. |
Beta Was this translation helpful? Give feedback.
-
The point of this post is not the syntax (or the math) because both are probably slightly weird or
wrong. The point is to put the general idea down in words.
Summary
and encode some timing behavior.
connections) between ports.
Examples
Consumer(T: TargetType, n: int)
: A reactor that acceptsn
inputs but produces no outputs.These reactors will generally have side effects such as writing to actuators or sending messages
over the network.
PeriodicProducer(T: TargetType, initial_offset: time, period: time)
: A timer is aPeriodicProducer
withT=void
. Such reactors as these may be useful for guaranteeing liveness.SporadicProducer(T: TargetType)
: A reactor that produces an output of type t at arbitrary times.A
PeriodicProducer
can be cast to aSporadicProducer
, but aSporadicProducer
cannot be castto a
PeriodicProducer
.SporadicProducerWithMinSpacing(T: TargetType, min_spacing: time)
: A reactor that behaves like aphysical action with a minimum spacing.
Function(InType: TargetType, OutType: TargetType)
: A reactor whose output is present at tag giff its input is present at g.
DelayedFunction(InType: TargetType, OutType: TargetType, delta_g: tag)
: A reactor whose outputis present at tag g + delta_g iff its input is present at g, where tag differences are added
elementwise. For all T, U, Function (T, U) = DelayedFunction(T, U, (0, 0))
PartialFunction(InType: TargetType, OutType: TargetType)
: A reactor whose output is not presentat tag g if its input is not present at g.
Motivation
In general, one reason why type annotations are valuable in a programming language is that they make
questions that could otherwise only be answered by a global view of the program possible to answer
using only a local view.
Causality interfaces are necessary in order to determine whether there are cycles. If causality
interfaces at the reactor level are implicit, a global view of the program is required in order to
determine whether there are cycles (and why). If they are explicit, then only the containing
reactor (where connections are made) need be inspected. This convenience may not be important for
a machine, but humans should be able to interpret how and why their programs have cycles, too.
Causality interfaces alone are insufficient to match the degree of static checking that exists in
popular statically typed languages.
f(x) := g(h1(x), h2(x))
, we write this:H0
andH1
are bothFunction
s. But what if one or both of them areDelayedFunction
s? Then their outputs may not be synchronized.G
will have to save whicheveroutput comes first so that it can merge it with the output that comes second. Alternatively, if
they are both
DelayedFunction
s with the same (precisely specified) delay, then again they willcertainly be synchronized. This use case is important because:
internally have pipelines (to maximize parallelism, and perhaps also to ensure correctness in
the case of hardware reactors with clock cycles that do not permit long combinatorial delays).
require iteration in order to compute some value. For example, the following function applies
a matrix to a vector many times, until the vector seems to be in an eigenspace. The number of
microsteps required for it to terminate is data-dependent and impossible to determine
statically.
whether a value is nullable is part of its type. The LF analogue of the Kotlin type
(input: Double) -> Int?
(a function that might return an integer or might returnnull
instead) isPartialFunction(Double, Int)
, for that is the type of a reactor that might or might notproduce a response to a request.
Causality interfaces alone are insufficient to summarize the deep timing analysis that LF has to
offer. (If I understand, MTL is the powerful "big hammer" for this purpose, but it might not be
the ideal choice everywhere?)
will produce a response to a request within 100 logical milliseconds, without looking at the
definitions of
R0
andR1
:part of the interfaces of components instead of logical times. I am not sure how that would
work.
PossiblyBoundedLag
reactor certainly does not have unbounded lag; however, the logical delayat least lets us determine that the program might have bounded lag without reading the source
code of
AddOneWithSmallInternalDelay
and its nested reactors.In order for reactors to be composed flexibly, they must specify the interfaces of reactors that
they can be parameterized by. The following is pseudocode (not allowed by our syntax):
Generalization
I will use the word "objects" to include ports, reactions, and triggers.
For brevity I will use the word "arrows" to refer to happens-before relations.
The following sets of arrows are closed under composition:
-> (0, 0) ?
-> (0, 0) !
-> (0, *) ?
-> (0, *) !
-> (*, *) ?
-> (*, *) !
-> (0, 4k)
The following sets of arrows are not closed under composition, but that's fine, for they are subsets
of the sets that are closed:
-> (0, 4) ?
-> (0, 4) !
-> (0, 2..9) ?
Of the arrows described here, those that we currently express explicitly are:
-> (0, 0) !
for connections between ports.-> (0, 0) ?
for arrows between a reaction's inputs and its outputs, and for the "causalinfluence" arrows between reactions in the same reactor. In addition,
-> (0, 0) !
arrows are asubset of the
-> (0, 0) ?
arrows. Many?
arrows could perhaps be turned into!
arrows usingthe target language parsing that Shaokai has been working on.
The
-> (0, 0) ?
arrows are the ones that are relevant to cycle detection.The rules for composing arrows are as you would expect: A
?
arrow composed with a!
arrow givesa
?
arrow, the parenthesized tag part "adds" elementwise, where*
plus anything is*
andranges such as
2..9
are the same as ordered pairs such as(2, 9)
that add elementwise.To represent the interface of a reactor, the user should specify one of the finite sets of arrows
that can generate all arrows. Here are some examples of trivial interface specifications:
To determine the interface of an arbitrary reactor, use the arrows that are specified explicitly in
the reactor to generate all arrows and then pick out the arrows between the reactor's input and
output ports, for those are the only ones that are relevant to the outside. In reactors with
infinitely many arrows, (as in the case of timers and self-loops), that algorithm will not work; for
this reason I have not figured out how to determine whether an arbitrary reactor with infinite
arrows implements an arbitrary interface in general.
A reactor of type A can be cast to type B if the
?
arrows in A are a subset of the?
arrowsin B and the
!
arrows in B are a subset of the!
arrows in A. As a reminder, all!
arrowsare
?
arrows, but not all?
arrows are!
arrows.Beta Was this translation helpful? Give feedback.
All reactions