Lambda the Ultimate

The issue isn't so much being able to model time. Many formalisms can do that. Nor is it about having access to 'real time'. Knowing the time is not the same as being able to respond in a timely manner. What Lee is interested in is designing systems that must interact with the physical world and therefore must have predictable, repeatable timing. His claim is that the standard abstractions we use to build computing systems (including actors) deliberately discard time as a part of their model, and that this makes it inherently difficult to build correct systems if those systems must interact with the physical world. Attempting to patch over the lack of time information by using something like an RTOS is a brittle and error-prone solution. Instead, Lee is proposing a change in the way computing is done, such that time is incorporated into our models from the ISA-level on up. He wants timing to be a core part of the semantics of programming languages.

What specifically is wrong, say, with what Ada provides? And if the issue is as you present it, why is this not the same as the requirements imposed on realtime systems?

Fundamentally, the problem is time as a step-function side-effect that isn't modeled, understood, or controlled by the programmer.

This makes for difficult composition. Two program fragments that may be individually correct might not be temporally correct when interleaved or placed in a sequence.

Strong timing means knowing and controlling how much 'time' takes place as a 'conceptual' side-effect of each operation.

This might not be the same as real-time, since one might simplify the model by saying that (for example) pure functions and Datalog queries take zero time, but that sending messages and accessing state take time. So long as one can 'fold' the functional operations into the time consumed by the state manipulation, a practical implementation may still be possible.

It may also be possible to enforce a 'perfect model' in the same sense as enforcing a 'perfect failure detector': if the model is wrong, kill enough processes to make it right again.

An accurate model of time, combined with strong timing, is necessary to analyze for real-time properties in the face of program composition.

I don't think Lee is looking too hard for a model of time accurate enough for realtime use. Any model of time that will help the programmers predict temporal behavior of programs would be appreciated.

As it turns out, Lee specifically addresses Ada (as well as other languages that incorporate some time information):

There is a long and somewhat checkered history of attempts to insert timing features into programming languages. Ada can express a delay operation, but not timing constraints. Real-Time Java augments the Java model with a few ad-hoc features that reduce variability of timing [7]. The synchronous languages [5], such as Esterel, Lustre, and Signal, do not have explicit timing constructs in them, but because of their predictable and repeatable approach to concurrency, can yield more predictable and repeatable timing than most alternatives. They are only limited by the underlying platform.

Lee also mentions several domain-specific languages (such as Simulink) that include temporal semantics, but asserts that they "...remain outside the mainstream of software engineering ... are not well integrated into software engineering processes and tools, and they have not benefited from many innovations in programming languages."

As I understand it, the requirements are those of real-time systems. However, Lee (and John Stankovic, whom he quotes) claim that "existing technology for RTES [real-time embedded systems] design does not effectively support the development of reliable and robust embedded systems." Specifically, Lee states that

Modern processor architectures render WCET virtually unknowable; even simple problems demand heroic efforts. In practice, reliable WCET numbers come with many caveats that are increasingly rare in software. Worse, any analysis that is done, no matter how tight the bounds are, applies to only a very specific program on a very specific piece of hardware. Any change in either the hardware or software, no matter how small, renders the analysis invalid. The processor ISA has failed to provide an adequate abstraction.

You're quite right that languages intended for real-time applications have in the past included some kind of temporal semantics. The problem is that modern processors make those semantics difficult (or impossible) to guarantee. Lee is suggesting a change in processor design (towards something like the Precision Timed Machine), with a corresponding change in the way the ISA is defined. The interesting question from a PL perspective is how those changes in the underlying platform should be reflected in higher-level language design. This paper gives a few pointers to the kind of issues that might need to be addressed in designing a language for such an architecture.

I was thinking of things like Rate Monotonic Analysis, and how support for it influenced the design of the language.

Interesting. I didn't realise that RMA was specifically considered in the design of Ada. What influence did it have on the language design?

Anyway, as I understand it, RMA only guarantees that a given set of tasks can be scheduled in a way that meets their deadlines. It doesn't guarantee that a particular implementation will actually execute scheduled tasks on deadline. I think that what Lee is getting at is that if the computing platform upon which your code is running is not sufficiently predictable as far as timing goes, you can end up with a system in which tasks may be properly-scheduled but are executed too late (or too early, which can be just as bad).

One approach to improving the predictability and repeatability of cache behaviour is to simplify the operation of the cache, and hand it over to programmer control. This paper describes one approach, sadly it didn't get much traction, hence it's not covered in the Precision Timed Machine paper when they describe the issue.

If the program specifies how the cache should behave, then the combined specification of program+caching is somewhat easier to analyse than program + generic cache behaviour.

Neat. Thanks for the pointer!

The independent nature of actors gives them a very personal view of time.
They know about before and after, yes, but what about simultaneity?
I believe that synchronous languages, such as Esterel and FRP, where the notion of time among entities is unique, is are much closer to Lee's rants.
Asynchronous concurrency (csp, actors, threads) are in oppose direction.
What do you think?

I often think of actor models as over reductions of most real physical processes. Physical systems such as the ubiquitus sampled data systems can only be abstracted by a computation. Typically this is a solution to some difference equation, a system with state. It is hard to think of an actor model equivalent. I tend to use the word activity instead. To be comfortable in a hybrid environment I would like a language with a formal semantics consistent with "sampled data semantics" or "clock semantics"

Some people may be interested to know that clock semantics actually has a modal logic definition. This is a recent summary with links to older results. Lax logic has been combined with effects in at least one formal language proposal previously mentioned on Ltu. A Modal Language for Effects.

I think dmbarbour has detailed one of many special cases dealing with timing. More subtly, his time model was designed to handle the inevitable timing errors that crop up.

I am not certain how any generalized strong timing framework will be useful without specifying how to handle timing errors. And, I can not see how handing timing errors can be done without knowing the specific domain the solution is for. Just like any robust application; the bulk of the code is dedicated to detecting and handing possible errors, not performing it’s main duty. For example, it is not enough to “guarantee” a method completes within 50ms. You also need to know what actions to take when this guarantee is broken.

Maybe once someone reviews enough specific domains they can see the general patterns used to deal with timing errors: I am not one of those people.

Lee brings up “…cars, medical devices, instruments, communication systems, industrial robots, toys, games…” which all must accept failure in particular ways. Each domain’s model of time will be different specifically to deal with *how* timing failure will be handled. Yes, some domains do not accept failure: and hardware solutions are required. But we all know that is overkill for the plethora of systems that would benefit from strong timing, but are a little more flexible with failure.

Having a framework for proper exception handing for timing failures allows us avoid the monetary cost of real hardware solutions to this problem. I contend it also solves the timing issues in a majority of the domains.

If we took this seriously, what would it look like?

My gut tells me that it is going to turn out to look very similar to parameterization constructs (i.e., polymorphic). Can anyone help flesh out this intuition?

An initial stab at a Time System, if I were aiming to achieve Strong Time Safety, would have the following basic timings, each of which could be associated with functions, procedures, methods... much like exception types or return types:

• unbounded: this method can take any amount of time, and might not even return.
• finite: this method is guaranteed to return after some finite, but unknown, amount of time. Similar to a termination guarantee, except that it might start events that never terminate... it just doesn't waits for them.
• progressive: finite and guaranteed to make progress towards termination in each quantum. (Wait-free.)
• processing bounded(Ti,Tf): this method is guaranteed to return (possibly in failure) after between [Ti,Tf] units processing time.
• absolute bounded(Ti,Tf): this method is guaranteed to return (possibly in failure) after between [Ti,Tf] units real-time.

For a realistic estimation of 'bounded' times, I would probably need dependent timing (similar to dependent typing). Static analysis of this would, of course, be a pain.

Calling patterns would be in layers. Unbounded calls can call anything. Finite calls can call anything but unbounded calls. Progressive calls can call anything but finite or unbounded calls. And so on.

Realtime would only be achieved with the most specific layers, which would be avoided outside of inner loops.

Strong timings could be attached both to 'interfaces' for black-box composition and still inferred for 'implementations'.

The language would provide asynchronous exceptions, timed promises and rendezvous, and various other constructs useful for programmers to control timing of events. In addition, constructs would exist for programmers to specify that events take place at specific times (e.g. starting in ten seconds, taking no more than 30 milliseconds, would be possible to define in this system).

For methods in an Actors Model system, I would rate by 'reply' time rather than event completion time. The two would only be the same for synchronous actors.

Anyhow, that's a sketch of how I'd do a timing system. Any other ideas?

One language I've recently read about, called Chuck, also calls itself Strongly Timed. It doesn't provide timings for procedures, though, and I don't believe it performs static analysis of any sort.

Karl Crary & Stephanie Weirich, 2000. Resource Bounded Certification. POPL #27.

This paper describes an approach to certifying that code respects time bounds using dependent type systems that express how long the code takes to run. They extend Typed Assembly Language in particular. to give the system they call TALres. I've not seen any work that builds on this approach.

As the authors say, there is no inference of time bounds for programs. One would have to mess about with the expressivity of a programming language to make that possible.

with all of the above. I just wanted to add that in this day and age if we did all that we would also want to consider power as a resource and avoid writing certain javascript/flash code that cooks your legs while browsing the Internet. Computing takes space, too, so if our software/data weren't that bloated, we'd have smaller hard drives as well.

we would also want to consider power as a resource and avoid writing certain javascript/flash code that cooks your legs while browsing the Internet

I could really benefit from that sort of analysis, as well as total energy cost analysis. Unmanned systems need as much power savings as they can achieve, and heat-management issues isn't unusual for unmanned systems either (we have vehicles running in Iraq with CPUs cooped up inside what are essentially ovens due to shuttering against sand).

I'd at least like automated "optimizations" for power and energy, but some sort of first-class analysis of these properties for systems engineering and program design would be very nice.

There are quite a few cross-cutting concerns like these. Languages have a lot more development to do.

I'm not nearly so pessimistic as you are on the possibilities of analysis and modeling for these issues, though I expect initial attempts will be more at the level of keeping programmers 'informed' of the costs of their decisions and helping with automatic analysis and optimizations - i.e. closer to 'soft temporal typing, soft energy typing, soft power typing' than to any hard variation.

We obviously cannot trust programming languages, at least if they permit Turing-complete code - as there is no way to truly verify the timing of such.

We really can get a LOT further without going Turing complete than we usually bother going in programming languages. We very rarely, if ever, need non-termination past non-termination of physical hardware/sensory input. Indeed, we probably want to do (in general) better than non-termination: for continuous sensor input, we really need to guarantee that the processing costs proportional to or smaller than the number of processors serving behalf of parties interested in each input times the number and size of inputs.

Avoiding Turing Complete operations: total functional programming, stratified logic languages (lacking infinite-fact-generator cycles) to ensure finite processing to determine or fail to determine any given fact, procedural languages that forbid arbitrary loop-backs (no 'while' loop, resumable exceptions limited to being forward of the throws statement). Certain call cycles among objects or actors could also be prevented, given a suitably limited object configuration language.

We can push 'Turing Complete' into the highest layer possible, maybe even to the outer edges, such that to have a Turing Complete program you literally need to involve physical hardware that bounces outputs back as as inputs at the very edges of the system. This isn't particularly unreasonable. How many object-configurations really need to support arbitrary cycles beyond physical input? Perhaps we should figure out which sort of limited cycles we'd most benefit from, and limit the language to just those.

Anyhow, giving up on a feature due to Turing Completeness, as though Turing Completeness is a feature rather than a largely unnecessary evil we suffer, tends to irk me a bit.

Your points on multi-tasking issues, interrupts and communications, etc. still apply, and are well taken. Even without being thwarted by Turing Completeness, accurate timing would be a difficult problem to whatever degree it needed to involve external resources.

The problem, though, is that many things that seem quite trivial are actually Turing-complete. For instance, various simple cellular automata, including not only Conway's Game of Life but also the 1-dimensional cellular automaton Rule 110, are actually Turing-complete. If one is not able to even implement Rule 110, physical hardware limitations such as memory space notwithstanding, then one must have actually imposed quite a great set of limitations upon oneself by not being Turing-complete.

Implementing the rules of such a simulation isn't what usually needs Turing-completeness - it's the unbounded update loop that does. You can usually structure things so that such loops are known at top-level. I'd expect timing requirements of such a simulation to usually be per-update. Also, a type system that maintains static bounds on run-times doesn't preclude the existence of an unbounded runtime type.

Once you start down the Turing Complete path, forever will it dominate your destiny, Matt.

While it is true we could provide an 'unbounded runtime type', we do not need one capable of introducing an unbounded update loop.

Instead, bind the update loop to an unbounded physical event-source, such as a periodic clock signal.

Not with a global operator, either, but rather as a capability that may be granted... such that clocks can can only be introduced from outside the language. There are many advantages (for reproducible testing) in denying direct access to physical resources.

Mostly I agree with you (which is the first part of what I said - expose the update loop as such at top level) - that's a better style. But I think it will sometimes be useful to write functions that we haven't proven to terminate without incorporating them into some framework for non-termination.

More to the point, my second comment was just addressing the logical possibility of having established time bounds on only a proper subset of the computations in your program.

But I think it will sometimes be useful to write functions that we haven't proven to terminate without incorporating them into some framework for non-termination.

That is the force of the Turing side whispering into your heart, Matt. You must be stronger... the temptation is strong, I know, but the using the Turing side of the force has a great cost that will topple empires.

And with a little less allusion, I expect you work primarily in an environment where the 'control loop' - and the ability to halt or kill it - is implicitly accessible via Operating System job control. That is not an assumption that scales well to secure, open, distributed systems with any form of automatic mobility, distribution, and self-healing.

In practice, though, I am sure if such formalism is really the best way attack the issue of timing that was originally brought up in the paper before it went the direction of saying that everything associated with general computing needs to be rebuilt from the ground up. Now that I think of it, probably the most effective way to approach this issue that could actually be done within present-day general computing, and which is most likely to actually be practically implemented, is the introduction of full (optionally hard) realtime facilities into general-purpose operating systems and user software actually taking advantage of such realtime facilities for things such as audio combined with the establishment of overall best practices for such things.

The idea of introducing (hard) realtime into general-purpose operating systems is not nearly as incompatible with the normal operation of general-purpose operating systems as one might think. All that it really requires is that specific processes be able to be scheduled in a realtime fashion, and for such realtime processes to be able to preempt not only any non-realtime process but also the kernel itself. Consequently if, say, a media application needs the ability to output audio or to be able to grab frames off the network or read data from fixed storage, decode any video or audio data, and output them using the video and audio systems, they will be able to do so in a smooth fashion regardless of outside non-realtime load provided that they take advantage of such realtime capabilities.

Of course, this would require other parts of the system to actually be realtime-aware rather that to treat realtimeness as something merely tacked into the side of the system. The video, audio, networking, and storage systems would all need to be able to expedite actions requested of them by realtime processes so as to handle media applications, to use the example from the paper; otherwise heavy loads from other processes could still impede any actions required by realtime processes that would be non-realtime in nature. Of course, there would be limitations to this - realtimeness cannot handle the fact that disks can only seek so fast and that disk access times are not predictable. However, for most user applications realtimeness would probably be less critical for storage than for video and audio (as if an application is reading video and audio data from a disk, the storage system could avoid latency problems by reading ahead).

You raise some interesting issues. But I don't think the picture is quite as bleak as you paint it. For starters, you could say much the same things about the functional correctness of computing systems:

We obviously cannot trust programming languages, at least if they permit Turing-complete code - as there is no way to truly verify [that they will even terminate, let alone produce a correct result.]

We obviously cannot trust programming languages (other than assembly) that have any more than one implementation [if those implementations don't conform to the language specifications], and if we use programming languages that have more than one implementation, we must code for a single exact implementation of such down to the exact version. Even upgrades to a compiler could change behavior, obviously.

We obviously cannot trust libraries, unless they are provided in an uncompiled state in a language that is not Turing-complete. [How can we possibly know what behavior a library will produce in the absence of fully verifiable source code?]

We obviously cannot have more than one application running at once, that is, we cannot trust any kind of multitasking involving outside code, as there is no way for us to control [the state of registers or memory] then. That also means that we cannot trust any kernel we have not written ourselves, as it may have behavior that we do not know [state-wise].

Yet somehow we manage to produce functionally correct software despite the potential problems.

You say "Simply having the same formal behavior is not enough, as such formal behavior clearly does not include actual exact timing behavior." But what if the timing behavior was part of the formal definition of behavior? If a language spec includes timing in its definition, then conforming compilers would presumably be required to ensure that the timing of a program remained consistent even if the compiler version changed (perhaps a new compiler version would have to add no-ops to ensure a particular lower-bound on execution, if that was what was required to provide the specified behavior). Giotto is one example of a system that's designed to allow both function and timing to be specified in a platform-independent way, and leaves it to the compiler to generate code that meets the timing constraints.

When it comes to libraries and multitasking OSes, maybe we need to rethink how those will work. Perhaps the ABI needs to include scheduling hooks or timing information. Perhaps the software installation process should include not just allocating disk or flash space but allocating schedule time. Perhaps we should allow a mixture of time-triggered tasks as well as reserved slots for contention amongst lower priority preemptive tasks. Perhaps we need to develop new techniques for dynamic scheduling of code that carries timing constraints with it. There's all sorts of interesting research to be done there.

Is the fundamental sea-change that Lee calls for really necessary? I'm not entirely sure, to be quite honest. Maybe we can continue to muddle along with layering "real-time" on top of time-free abstractions. But I think it's worth at least considering what the alternative might look like, and what it would buy us.

You raise some interesting issues. But I don't think the picture is quite as bleak as you paint it. For starters, you could say much the same things about the functional correctness of computing systems:

[...]

Yet somehow we manage to produce functionally correct software despite the potential problems.

This is because there are means of producing sufficiently well-functioning software other than relying on formalisms to enforce correctness. In reality, such is achieved through various software development practices, which largely allow us to create functionally correct software without such.

You say "Simply having the same formal behavior is not enough, as such formal behavior clearly does not include actual exact timing behavior." But what if the timing behavior was part of the formal definition of behavior? If a language spec includes timing in its definition, then conforming compilers would presumably be required to ensure that the timing of a program remained consistent even if the compiler version changed (perhaps a new compiler version would have to add no-ops to ensure a particular lower-bound on execution, if that was what was required to provide the specified behavior). Giotto is one example of a system that's designed to allow both function and timing to be specified in a platform-independent way, and leaves it to the compiler to generate code that meets the timing constraints.

The problem with enforcing exact timing down to the specification level is that we inevitably would have to enforce it right all the way down to the metal, and would most definitely have to enforce it at the operating system, compiler, and language runtime levels. The problem with such, though, is that hardware, operating systems, compilers, and language runtimes could never become better; the timing would be part of the platform itself, so one could never make a better processor core, or a better cache, or better DRAM, or a better scheduler, or a better compiler, or a better runtime. One would be bound to the timing specified when a platform was originally created until the time at which it would finally be obsoleted. And while this may be well and good for embedded applications or gaming consoles, this is certainly not acceptable for open general computing platforms.

When it comes to libraries and multitasking OSes, maybe we need to rethink how those will work. Perhaps the ABI needs to include scheduling hooks or timing information. Perhaps the software installation process should include not just allocating disk or flash space but allocating schedule time. Perhaps we should allow a mixture of time-triggered tasks as well as reserved slots for contention amongst lower priority preemptive tasks. Perhaps we need to develop new techniques for dynamic scheduling of code that carries timing constraints with it. There's all sorts of interesting research to be done there.

Is the fundamental sea-change that Lee calls for really necessary? I'm not entirely sure, to be quite honest. Maybe we can continue to muddle along with layering "real-time" on top of time-free abstractions. But I think it's worth at least considering what the alternative might look like, and what it would buy us.

I myself just think that the most practical approach which would actually work is to build realtime into general computing platforms from the ground up and to take it seriously rather than to merely tack it on as an afterthought or niche function. That is, not to merely have a realtime capacity at the kernel or even a preemptable kernel, but to construct all basic level system services (whether in kernel space or user space) and libraries to support realtime operation - that is, the kernel and userland would have to be fundamentally capable of realtime operation themselves. Most applications will not need realtime, but those which will need it, such as video and audio-related applications and certain sorts of networking applications (such as voice over IP and packet filtering) will need to be able to take full advantage of realtimeness without being hampered by system services and libraries not fully designed for it. And while such may seem radical in the sense that it will require significant changes at the kernel and userland levels to any operating system being modified to fit such, it actually would be very conservative in impact, and would have practically no impact upon normal general computing outside operating system design and implementation.

This is because there are means of producing sufficiently well-functioning software other than relying on formalisms to enforce correctness.

The problem with such, though, is that hardware, operating systems, compilers, and language runtimes could [i]never become better[/i]; the timing would be part of the platform itself, so one could never make better DRAM, or a better cache, or a better scheduler, or a better compiler, or a better runtime. One would be bound to the timing specified when a platform was originally created until the time at which it would finally be obsoleted.

I myself just think that the most practical approach which would actually work is to build realtime into general computing platforms from the ground up and to take it seriously rather than to merely tack it on as an afterthought or niche function. ... construct all basic level system services (whether in kernel space or user space) and libraries to support realtime operation.

Really? You don't think that things like calling conventions, static analyses, type systems, memory protection, modular programming, or other ways of "enforcing" correctness have helped?

They most certainly have. I was more talking about formal code verification, where one can prove that code is correct or, in this case, that its timing is correct.

That rather depends on what you mean by "better", doesn't it? You seem to be implicitly equating "better" with "faster". But better can also mean "more predictable", "uses less silicon", "consumes less memory", "uses less battery power", "suffers less timing jitter". Furthermore, there's nothing to prevent you from having "better" mean "faster" so long as (for example) your compiler or runtime was made aware of the change in timing of the underlying ISA and was able to compensate approriately to maintain the specified timing constraints of existing programs.

"Faster" was implicit in my comment there, yes. But what I was saying is that you could never make any future changes that change timing behavior, regardless of the merits of such changes. Hence you would be bound to the originally specified timing behavior, regardless of the merits of any future developments - and that such is not acceptable for general computing.

In a sense, that's precisely what Lee is suggesting. He's just arguing that to do it right requires processor architectures designed with timing in mind. But as with your suggestion, once the capabilities are in place, there's no requirement that you use them.

He was also saying that we would need to completely replace all existing operating system and language paradigms as well, whereas I was saying that with proper realtime support at the operating system level, one could have systems that would look essentially the same as before from without to non-realtime applications. One would not need to even discard things such as POSIX and garbage collection for the normal non-realtime application, but rather would just need to specify a practical realtime API which would allow applications that do need realtimeness to run without interference from non-realtime applications. (Such could range from anything like a special realtime scheduling API combined with system services that actually use it to a full realtime microkernel system on which POSIX is but one API provided by a set of runtime libraries and servers.)

tutorial says "An other hypothesis is that computations take a null time. So we consider that new values are produced at the same logical instant as data used in their computation."

which made me raise my eyebrows.

on the other hand, i think it would be very hard to predict for how long any given routine will run. :-)

as i was reading i kept thinking thoughts that you then summarized in your last paragraph :-) since i grew up on 6502/10 and z80. :-)

We can have global time with only local state.

In practice, you'll still have `global` shared state resources anyway, such as databases and distributed hashtables.