search

jepsen-io / jepsen

A framework for distributed systems verification, with fault injection
6.78k stars 715 forks source link

Linear analyse problem #432

Closed wfystx closed 4 years ago

wfystx commented 4 years ago 
:final-paths
  ([{:op
     {:process 4,
      :type :ok,
      :f :write,
      :value 4,
      :index 35279,
      :time 394925843615},
     :model {:value 4}}
    {:op
     {:process 3,
      :type :ok,
      :f :read,
      :value 1,
      :index 35282,
      :time 394985253044},
     :model {:msg "4≠1"}}]
   [{:op
     {:process 4,
      :type :ok,
      :f :write,
      :value 4,
      :index 35279,
      :time 394925843615},
     :model {:value 4}}
    {:op
     {:process 1,
      :type :invoke,
      :f :read,
      :value 4,
      :index 35264,
      :time 394736854607},
     :model {:value 4}}
    {:op
     {:process 3,
      :type :ok,
      :f :read,
      :value 1,
      :index 35282,
      :time 394985253044},
     :model {:msg "4≠1"}}]),
  :previous-ok
  {:process 0,
   :type :ok,
   :f :write,
   :value 1,
   :index 35280,
   :time 394942538345},
  :last-op
  {:process 4,
   :type :ok,
   :f :write,
   :value 4,
   :index 35279,
   :time 394925843615},
  :op
  {:process 3,
   :type :ok,
   :f :read,
   :value 1,
   :index 35282,
   :time 394985253044},
  :analyzer :linear},
 :valid? false}

Analysis invalid! (ﾉಥ益ಥ）ﾉ ┻━┻

The log above seems believe that the expected value should 4 instead of 1. But I got confused after I checked the history.

{:type :invoke, :f :write, :value 1, :process 0, :time 394737291082, :index 35265}
{:type :invoke, :f :read, :value nil, :process 2, :time 394767185191, :index 35266}
{:type :ok, :f :read, :value 1, :process 2, :time 394768172241, :index 35267}
{:type :invoke, :f :write, :value 1, :process 4, :time 394808094183, :index 35268}
{:type :ok, :f :write, :value 1, :process 4, :time 394810364751, :index 35269}
{:type :invoke, :f :read, :value nil, :process 4, :time 394810547341, :index 35270}
{:type :ok, :f :read, :value 1, :process 4, :time 394811337269, :index 35271}
{:type :invoke, :f :read, :value nil, :process 2, :time 394815457021, :index 35272}
{:type :ok, :f :read, :value 1, :process 2, :time 394816386168, :index 35273}
{:type :invoke, :f :read, :value nil, :process 3, :time 394830098886, :index 35274}
{:type :ok, :f :read, :value 1, :process 3, :time 394831088041, :index 35275}
{:type :invoke, :f :read, :value nil, :process 2, :time 394916677135, :index 35276}
{:type :ok, :f :read, :value 1, :process 2, :time 394917581284, :index 35277}
{:type :invoke, :f :write, :value 4, :process 4, :time 394923593767, :index 35278}
{:type :ok, :f :write, :value 4, :process 4, :time 394925843615, :index 35279}
{:type :ok, :f :write, :value 1, :process 0, :time 394942538345, :index 35280}
{:type :invoke, :f :read, :value nil, :process 3, :time 394984365282, :index 35281}
{:type :ok, :f :read, :value 1, :process 3, :time 394985253044, :index 35282}

Here is the history. I think there should be no problem. Am I understanding it in a wrong direction?

aphyr commented 4 years ago

Naw, this looks reasonable to me. Could depend on what happened before, but look at the linearization point for process 0's write of 1: it's likely gotta be immediately after invocation, which rules out using it to reach 1 after the write of 4.On Jan 8, 2020 23:56, Fuyao Wang notifications@github.com wrote::final-paths

([{:op

 {:process 4,

  :type :ok,

  :f :write,

  :value 4,

  :index 35279,

  :time 394925843615},

 :model {:value 4}}

{:op

 {:process 3,

  :type :ok,

  :f :read,

  :value 1,

  :index 35282,

  :time 394985253044},

 :model {:msg "4≠1"}}]

[{:op

 {:process 4,

  :type :ok,

  :f :write,

  :value 4,

  :index 35279,

  :time 394925843615},

 :model {:value 4}}

{:op

 {:process 1,

  :type :invoke,

  :f :read,

  :value 4,

  :index 35264,

  :time 394736854607},

 :model {:value 4}}

{:op

 {:process 3,

  :type :ok,

  :f :read,

  :value 1,

  :index 35282,

  :time 394985253044},

 :model {:msg "4≠1"}}]),

:previous-ok

{:process 0,

:type :ok,

:f :write,

:value 1,

:index 35280,

:time 394942538345},

:last-op

{:process 4,

:type :ok,

:f :write,

:value 4,

:index 35279,

:time 394925843615},

:op

{:process 3,

:type :ok,

:f :read,

:value 1,

:index 35282,

:time 394985253044},

:analyzer :linear},

:valid? false}

Analysis invalid! (ﾉಥ益ಥ）ﾉ ┻━┻

The log above seems believe that the expected value should 4 instead of 1. But I got confused after I checked the history.

{:type :invoke, :f :write, :value 1, :process 0, :time 394737291082, :index 35265}

{:type :invoke, :f :read, :value nil, :process 2, :time 394767185191, :index 35266}

{:type :ok, :f :read, :value 1, :process 2, :time 394768172241, :index 35267}

{:type :invoke, :f :write, :value 1, :process 4, :time 394808094183, :index 35268}

{:type :ok, :f :write, :value 1, :process 4, :time 394810364751, :index 35269}

{:type :invoke, :f :read, :value nil, :process 4, :time 394810547341, :index 35270}

{:type :ok, :f :read, :value 1, :process 4, :time 394811337269, :index 35271}

{:type :invoke, :f :read, :value nil, :process 2, :time 394815457021, :index 35272}

{:type :ok, :f :read, :value 1, :process 2, :time 394816386168, :index 35273}

{:type :invoke, :f :read, :value nil, :process 3, :time 394830098886, :index 35274}

{:type :ok, :f :read, :value 1, :process 3, :time 394831088041, :index 35275}

{:type :invoke, :f :read, :value nil, :process 2, :time 394916677135, :index 35276}

{:type :ok, :f :read, :value 1, :process 2, :time 394917581284, :index 35277}

{:type :invoke, :f :write, :value 4, :process 4, :time 394923593767, :index 35278}

{:type :ok, :f :write, :value 4, :process 4, :time 394925843615, :index 35279}

{:type :ok, :f :write, :value 1, :process 0, :time 394942538345, :index 35280}

{:type :invoke, :f :read, :value nil, :process 3, :time 394984365282, :index 35281}

{:type :ok, :f :read, :value 1, :process 3, :time 394985253044, :index 35282}

Here is the history. I think there should be no problem.

Am I understanding it in a wrong direction?

—You are receiving this because you are subscribed to this thread.Reply to this email directly, view it on GitHub, or unsubscribe.

wfystx commented 4 years ago

Thanks