Physical vs Logical Time

submited by

Style Pass

2021-06-22 08:30:04

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:

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.