jepsen-io / knossos

Verifies the linearizability of experimentally accessible histories.
398 stars 31 forks source link

Is this an non linearizable result? #16

Closed gaodq closed 6 years ago

gaodq commented 6 years ago

Hi, Kyle I have got an non linearizable result according to jepsen as the following figure. But I guess this is a linearization, there is an order of 0 read 1, 2 read 1, 3 read 1, 4 read 1, 1 write 0 Am I wrong? or this is bug?

aphyr commented 6 years ago

Without the history I can't tell you, but I think if you look at the full history or analysis results you'll discover that the write of 0 had to complete before the reads of 1. The visualization doesn't show the full history, just the part where things specifically went wrong.

gaodq commented 6 years ago

Thanks for your reply, but it's really a difficult work to find the wrong part from full history, is there any shortcut?

gaodq commented 6 years ago

I see, the 'index' in 'results.edn' is the line number in 'history.txt' I got this part from full history:

   1  3 :invoke :read nil
   2 4 :invoke :read nil
   3 2 :invoke :read nil
   4 1 :invoke :write  0
   5 0 :invoke :read nil
   6 1 :ok :write  0              <-----
   7 3 :ok :read 1
   8 0 :ok :read 1
   9 2 :ok :read 1
  10 4 :ok :read 1
  11 1 :invoke :write  1
  12 2 :invoke :write  4

Here is my results.edn and history.txt attachment. full_history.zip

aphyr commented 6 years ago

On vacation with only a phone at the moment but I'll look when I'm back in a few weeks or so.--KyleOn Sep 9, 2017 16:27, Gao Dunqiao notifications@github.com wrote:I see, the 'index' in 'results.edn' is the line number in 'history.txt' I got this part from full history: 1 3 :invoke :read nil 2 4 :invoke :read nil 3 2 :invoke :read nil 4 1 :invoke :write 0 5 0 :invoke :read nil 6 1 :ok :write 0 <----- 7 3 :ok :read 1 8 0 :ok :read 1 9 2 :ok :read 1 10 4 :ok :read 1 11 1 :invoke :write 1 12 2 :invoke :write 4

Here is my results.edn and history.txt attachment. full_history.zip

—You are receiving this because you commented.Reply to this email directly, view it on GitHub, or mute the thread.