June 21, 2021

Physical vs Logical Time

There's nothing I'm rarin' to share so I figured I'd talk about a concept in verification I see a lot but haven't seen explicitly discussed anywhere. I don't think this is revolutionary or anything but you might find it a useful heuristic.

---

There are two kinds of time in a system. The first is physical time, which is what most people think of as "time". Physical time is duration something takes to run. Logical time is the abstract division of the system into epochs. A system belongs to two separate epochs if there's a "before" and "after" that occupy different places in the state space. That means there is some query that returns different results for the same parameters. Usually physical and logical time are correlated, but not always:

• If I run a SQL SELECT that takes ten seconds to complete, then that's ten seconds of physical time. If that doesn't change the database, then no "logical time" has passed: there is no query that can differentiate "before the SELECT" and "after the SELECT".
• If I sort an array in-place, it can potentially take much less physical time than creating a new array, but it's not atomic, so creates many epochs in logical time.

Logical time is contextual. If the database caches the query, then you can identify the new epoch by how long queries take. In some cases, this matters a lot, while in others, we only care about the results of queries, so it's still the same epoch. In the absence of concurrency or aliasing, in-place sorting is behaviorally indistinguishable from returning a new sorted array, so logical time is the same. In a concurrent system, each agent has its own Lamport clock and logical time progresses at different rates.

Logical time matters to system correctness. Mutation and logical time are the same thing: if the system mutates, we can query that, so it's a different epoch. And if we're in a new epoch, we can measure something different, so some state must have changed. Since queries change for every epoch, we need to minimize the number of epochs if we want to reason about system correctness, such as by using database transactions. Two consequences of this:

1. Logical time is less relevant to single-threaded, non-concurrent programs, as nothing's querying them. It still matters, just less. This is a reason why people underestimate concurrent programming: something that used to be easy is now a fundamental challenge.
2. "Mutation" doesn't just mean local program values, it includes anything that changes the queryable system state. Changing values in a database counts as mutation, even if the code changing it is totally stateless. We need to minimize the number of global epochs.

Cache Invalidation

Cache invalidation is hard because it couples physical time and logical time. Each cache write corresponds to four epochs:

1. The cache is empty
2. The cache is written
3. The cache is outdated (the "danger zone")
4. The cache is invalidated.

The ideal caching system needs to maximize the physical time we spend in epoch (2) and minimize the time in (3). We don't have control over when the mutation happens and can only partially predict it. There are other challenges to cache invalidation, but this is the essential one: it comes from the definition of the problem and not the specifics of our technology.

(Not to mention that we introduce caching in the first place to address resource constraints… like physical time! Resource constraints are one of the biggest sources of complexity in programming and I'm surprised I've seen so little discussion of the interplay between constraints and functional requirements. Someone who knows more about this than me should write something.

(Also it's now called "Constraint Driven Development" no takesies backsies)

State Machines

State machines formalize logical time. While epochs corresponds to state changes, in state machines they also correspond to state transitions. The logic clock timeline is also an event timeline. This can rule out unexpected ticks. State machines are super common in formal verification, both as a way to organize individual programs and as a way to organize larger systems. Note you can have state in addition to the state machine states, like if you have three state machine states and a counter: int state. Maybe it's more manageable if you only update the data state when you transition between state machine states? state state state

Conclusion

Time sucks and I hate it

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.