Could I check a history that with real-time order about elle HOT 7 CLOSED

from elle.

Sorry, maybe I didn't describe it clearly. What I want to construct is a lost-update anomaly.
Suppose the 3 transactions as t1, t2 t3. I set t3 start only after t1 and t2 commit., soe have the execution satisfies

commitTs(t1) < startTs(t3)
commitTs(t2) < startTs(t3)

The full history is here

{:process 0, :f :txn, :part true, :value [[:start-txn nil true] [:r 0 0]], :time 216149557, :type :ok, :index 15}
{:process 1, :f :txn, :part true, :value [[:start-txn nil true] [:w 0 2]], :time 241574330, :type :ok, :index 24}
{:process 1, :f :txn, :part true, :value [[:commit-txn nil true]], :time 1255571934, :type :ok, :index 46}
{:process 0, :f :txn, :part true, :value [[:w 0 1] [:commit-txn nil true]], :time 1273574209, :type :ok, :index 60}
{:process 3, :f :txn, :part false, :value [[:r 0 1]], :time 1283358766, :type :ok, :index 68}

It is right that one valid serializable schedule is <t1, t3, t2>, but t3 happens last actually.
It's like both t1 and t2 execute in the morning and t3 execute in the evening.

We only consider t1 and t2.

• If t1 happens before t2, we should read 2 in t3.
• if t2 happens before t1, we should read 2 in t1.

So the execution is neither <t1, t2, t3> nor <t2, t1, t3>.

It is an anomaly, but it is really hard to describe.

from elle.

This history is still serializable though. That's what serializability means--equivalence to some ordering of transactions.

from elle.

Thanks, I will close this issue.

from elle.

If you're asking if it's strict serializable... the answer is no, and Elle should, I think be able to detect this. Did you try it?

from elle.

I will take a try, thank you very much.

from elle.

(Whether it can detect a realtime violation with a read-write register might depend on the strength of the per-key version order inference; I'm not sure off the top of my head whether a linearizable-key or WFR assumption is sufficient here. Should definitely work with a list-append workload though!)

from elle.