How fine-grained can the time hierarchy theorem be in a reasonable model?

One version of the sharp or additive space hierarchy theorem is that for Turing machines (and a number of other deterministic sequential computational models) $\mathrm{Space}(f-ω(\log(n+f))) ⊊ \mathrm{Space}(f)$ for space-constructible $f(n)$, where space is measured in bits.

Are there reasonable computational models where we have an analogous sharp version of the time hierarchy theorem: $\mathrm{Time}(f+O(1)) ⊊ \mathrm{Time}(f+O(g))$ for $g$-time-computable $f(n)$ with $g(n)≥\log(n+f(n))$?

Since I already know one (arguably reasonable) class of models with the sharp time hierarchy, I am including it as an answer, but I am still interested in related results, including
- other models with the sharp time hierarchy theorem
- whether this model or other models were studied in literature
- weaker forms of time hierarchy, especially if stronger than $\mathrm{Time}(f) ⊊ \mathrm{Time}((1+ε)f)$
- whether there is a speed-up theorem for Turing machines with a fixed number of binary tapes that would prevent this form of sharp time hierarchy.

Footnotes/References:
* The additive/sharp space hierarchy theorem can proved using "Halting Space-Bounded Computations" by Michael Sipser (1978). See also "Improved time and space hierarchies of one-tape off-line TMs" by Kazuo Iwama and Chuzo Iwamoto (1998).
* A weak form of additive time hierarchy is discussed in "Computational Models with No Linear Speedup" by Amir Ben-Amram, Niels Christensen, Jakob Grue Simonsen (2012).

The three ingredients of a diagonalization based proof of the time hierarchy theorem are universal simulation, timing, and reversal. By choosing (or defining) a computational model where these operations are efficient, we get a sharp hierarchy theorem. In particular, by using a model with a timed virtualization primitive satisfying certain conditions, we get a time hierarchy in the requested form. However, unlike the sharp space hierarchy, the precise time usage and hierarchy is on a per-model basis (and thus somewhat arbitrary).

If we set up things appropriately, the following algorithm can be implemented in time $f(n)+O(g(n))$ but not in time i.o.-$(f(n)+O(1))$ where $g(n)≥\log(n+f(n))$ and $f$ is $g$-time computable (i.o. means infinitely often):
* Determine the input length $n$, and compute $f(n)$.
* Read a small portion of the input to get a code $M$.
* Run TimedVirtualize($M$, $f(n) + \lg(n)$)  # check whether $M$ accepts the input in $f(n) + \lg(n)$ steps; TimedVirtualize must be fast enough.
* If $M$ accepts, then Reject, and otherwise Accept.

For the time hierarchy, the simplest model is to have a special tape to write the parameters, and an instruction to call TimedVirtualize with a mapping: {Accept, Reject,Timeout}→{Accept,Reject,Timeout} (with no further instructions after TimedVirtualize finishes; TimedVirtualize runs in real time).

However, it is more natural to be able to use virtualization repeatedly, and the rest of the answer gives a partial specification of a class of timed virtualization models, and how such a model can be implemented efficiently.

Timed Virtualization

A computational model defines how a program is interpreted and how much time it takes. A problem is solvable in time $f$ iff some program solves in time $f(n)$ for all valid inputs where $n$ is the input length. We assume that input length can be determined in logarithmic time.

One approach to timed virtualization is to use code, data, and privileged data 'tapes'. The code tape need not be directly accessible. The data and privileged data tapes are accessible, except that at a given time, a portion of the privileged data tape may be invisible and undetectable. In addition to ordinary instructions, the models have a virtualization function
TimedVirtualize(Code, Time) such that:

1. The machine executes Code for up to Time steps (Code and Time are obtained from the privileged data tape). The code is executed and each step is counted as if we initially set the code to Code (and the data tape to its current state.) All instructions (including TimedVirtualize) are permitted. The code sees the privileged data tape as initially empty. The previous privileged data remains unchanged (but the hierarchy theorems would also hold if it were erased instead).

2. TimedVirtualize returns a value coding Timeout/Accept/Reject depending on whether the code timed out or called an Accept/Reject instruction (that would otherwise Accept/Reject the input).

3. (optional extension) an optional space bound can be set.

4. Full-speed condition: The number of steps TimedVirtualize(Code, Time) takes equals the number of steps Code took (which is ≤Time), plus Time-independent overhead, plus $O(\log(\mathrm{Time}))$.

5. A number of features can be added to TimedVirtualize, but they are not needed for the hierarchy theorems. For example, we might want to set initial privileged data, get the time spent by Code, allow unbounded time, or (optionally) do nonvirtualized execution that replaces the code and (visible) privileged data (thus saving space).

Under basic assumptions about the code and timings, every model of this type satisfies the sharp time hierarchy theorem. The computation of $f(n)$ must erase the worktape at the end (except for the input data if do not use a read-only input tape); we can either define time-constructibility to include the erasure, or use a model where the erasure can be done in linear time.

Efficient Example and Implementation

For every $k$, there is such a model that can simulate in linear time $k$-tape Turing machines (time depends on the machine simulated), and in turn can be simulated in linear time by a $k+2$-tape Turing machine, which suggests that the full-speed condition is computationally reasonable. (Since a model defines timings, an implementation is an important evidence of reasonableness.) I am not sure if the two tape gap can be reduced to 0.

To get such a model, we fix an interpretation and timings of the code such that an efficient universal Turing machine can simulate the code in linear time, with the constant factor independent of the code size. For example, we can interpret the code as a Turing machine, but with the state transition specifying the relative offset $d$ (in bits) and taking $k(d+1)$ time, and with a convention and timings for TimedVirtualize (also, note that without random access tapes, head/cursor position is important). In addition to the tapes in the model, the machine uses a tape storing the timers (and if implemented, space bounds). While at time $t$, we might have $O(t / \log t)$ timers, we only need the antimonotonic case (timers that are set later trigger sooner), so we can use a counter for the innermost timer, and efficiently use subtraction to update the previous timer when TimedVirtualize finishes.

TimeSpace Hierarchy

If we define space usage in a reasonable way (and allow space bounds in virtualization), we can even get models with a sharp TimeSpace hierarchy theorem: $\mathrm{TimeSpace}(T+O(1), S+O(1)) ⊊ \mathrm{TimeSpace}(T+O(g), S+h+O(\log T))$ for $\mathrm{TimeSpace}(g,h)$-constructible $(T,S)$ with $g(n)≥\log(n)$ and $T(n)≥n$. The need for precise timings makes the space hierarchy less sharp here (at least to the extent we can currently prove the hierarchy).