Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Model failure: Unexpected cancel timer #23

Closed
jlouis opened this issue Sep 2, 2016 · 3 comments
Closed

Model failure: Unexpected cancel timer #23

jlouis opened this issue Sep 2, 2016 · 3 comments

Comments

@jlouis
Copy link
Owner

jlouis commented Sep 2, 2016 

Shrinking xxxxxx.xx.x.x.xxx.xx.x..x.x.xxxx...x...xxxxx(16 times)
[{set,
  {var,1},
  {call,fuse_eqc,install,
   [phineas,{{fault_injection,1.0e-19,1,1},{reset,1}}],
   [{id,1},
    {self,{var,{pid,root}}},
    {res,ok},
    {callouts,
     {seq,
      [{seq,
        [{callout,fuse_time,convert_time_unit,[1,milli_seconds,native],1},
         {return,1}]},
       {seq,
        [{internal,fuse_eqc,install_fuse,
          [phineas,
           {phineas,
            {fuse,
             {fault_injection,1.0e-19},
             1,1,ok,undefined,
             [{delay,1}],
             false}}],
          [{id,1},{self,{var,{pid,root}}}],
          empty},
         {seq,
          [{internal,fuse_eqc,clear_blown,
            [phineas],
            [{id,1},{self,{var,{pid,root}}}],
            empty},
           {seq,
            [{internal,fuse_eqc,clear_melts,
              [phineas],
              [{id,1},{self,{var,{pid,root}}}],
              empty},
             {return,ok}]}]}]}]}}]}},
 {set,
  {var,2},
  {call,fuse_eqc,melt_installed,
   [phineas],
   [{id,18},
    {self,{var,{pid,root}}},
    {res,ok},
    {callouts,
     {seq,
      {res,
       {internal,fuse_time_eqc,monotonic_time,[],
        [{id,18},{self,{var,{pid,root}}}],
        {seq,[{callout,fuse_time,monotonic_time,[],0},{return,0}]}},
       0},
      {seq,
       [{seq,
         [{internal,fuse_eqc,record_melt,
           [phineas,0],
           [{id,18},{self,{var,{pid,root}}}],
           empty},
          {seq,
           {res,
            {internal,fuse_eqc,fuse_period,
             [phineas],
             [{id,18},{self,{var,{pid,root}}}],
             empty},
            1},
           {seq,
            [{internal,fuse_eqc,expire_melts,
              [phineas,1,0],
              [{id,18},{self,{var,{pid,root}}}],
              empty},
             empty]}}]},
        {return,ok}]}}}]}},
 {set,
  {var,3},
  {call,fuse_eqc,melt_installed,
   [phineas],
   [{id,19},
    {self,{var,{pid,root}}},
    {res,ok},
    {callouts,
     {seq,
      {res,
       {internal,fuse_time_eqc,monotonic_time,[],
        [{id,19},{self,{var,{pid,root}}}],
        {seq,[{callout,fuse_time,monotonic_time,[],0},{return,0}]}},
       0},
      {seq,
       [{seq,
         [{internal,fuse_eqc,record_melt,
           [phineas,0],
           [{id,19},{self,{var,{pid,root}}}],
           empty},
          {seq,
           {res,
            {internal,fuse_eqc,fuse_period,
             [phineas],
             [{id,19},{self,{var,{pid,root}}}],
             empty},
            1},
           {seq,
            [{internal,fuse_eqc,expire_melts,
              [phineas,1,0],
              [{id,19},{self,{var,{pid,root}}}],
              empty},
             {internal,fuse_eqc,blow_fuse,
              [phineas],
              [{id,19},{self,{var,{pid,root}}}],
              {seq,
               [{internal,fuse_eqc,add_blown,
                 [phineas],
                 [{id,19},{self,{var,{pid,root}}}],
                 empty},
                {seq,
                 {res,
                  {internal,fuse_eqc,next_command,
                   [phineas],
                   [{id,19},{self,{var,{pid,root}}}],
                   {return,{delay,1}}},
                  {delay,1}},
                 {seq,
                  {res,
                   {internal,fuse_time_eqc,send_after,
                    [1,'_',{reset,phineas}],
                    [{id,19},{self,{var,{pid,root}}}],
                    {seq,
                     [{callout,fuse_time,send_after,
                       [1,'_',{reset,phineas}],
                       {tref,0}},
                      {return,{tref,0}}]}},
                   {tref,0}},
                  {seq,
                   [empty,
                    {internal,fuse_eqc,add_timer,
                     [phineas,{tref,0}],
                     [{id,19},{self,{var,{pid,root}}}],
                     empty}]}}}]}}]}}]},
        {return,ok}]}}}]}},
 {set,
  {var,4},
  {call,fuse_eqc,install,
   [phineas,{{fault_injection,1.0e-19,1,1},{reset,1}}],
   [{id,23},
    {self,{var,{pid,root}}},
    {res,ok},
    {callouts,
     {seq,
      [{seq,
        [{callout,fuse_time,convert_time_unit,[1,milli_seconds,native],1},
         {return,1}]},
       {seq,
        [{internal,fuse_eqc,install_fuse,
          [phineas,
           {phineas,
            {fuse,
             {fault_injection,1.0e-19},
             1,1,ok,undefined,
             [{delay,1}],
             false}}],
          [{id,23},{self,{var,{pid,root}}}],
          empty},
         {seq,
          [{internal,fuse_eqc,clear_blown,
            [phineas],
            [{id,23},{self,{var,{pid,root}}}],
            empty},
           {seq,
            [{internal,fuse_eqc,clear_melts,
              [phineas],
              [{id,23},{self,{var,{pid,root}}}],
              empty},
             {return,ok}]}]}]}]}}]}}]

S: [{fuse_time_eqc, {state, 0, [], 0}},
    {fuse_eqc, {state, [], []}}]


fuse_eqc:install(phineas, {{fault_injection, 1.0e-19, 1, 1}, {reset, 1}}) ->
  1 = fuse_time:convert_time_unit(1, milli_seconds, native),
  ok.

S: [{fuse_time_eqc, {state, 0, [], 0}},
    {fuse_eqc,
       {state, [],
          [{phineas,
              {fuse, {fault_injection, 1.0e-19}, 1, 1, ok, undefined,
                 [{delay, 1}], false}}]}}]


fuse_eqc:melt_installed(phineas) ->
  0 = fuse_time:monotonic_time(),
  ok.

S: [{fuse_time_eqc, {state, 0, [], 0}},
    {fuse_eqc,
       {state, [{phineas, 0}],
          [{phineas,
              {fuse, {fault_injection, 1.0e-19}, 1, 1, ok, undefined,
                 [{delay, 1}], false}}]}}]


fuse_eqc:melt_installed(phineas) ->
  0 = fuse_time:monotonic_time(),
  {tref, 0} = fuse_time:send_after(1, <0.10943.2>, {reset, phineas}),
  ok.

S: [{fuse_time_eqc,
       {state, 0, [{1, 0, '_', {reset, phineas}}], 1}},
    {fuse_eqc,
       {state, [{phineas, 0}, {phineas, 0}],
          [{phineas,
              {fuse, {fault_injection, 1.0e-19}, 1, 1, {blown, []}, {tref, 0},
                 [{delay, 1}], false}}]}}]


fuse_eqc:install(phineas, {{fault_injection, 1.0e-19, 1, 1}, {reset, 1}}) ->
  1 = fuse_time:convert_time_unit(1, milli_seconds, native),
  exit({mocking_error, unexpected}) = fuse_time:cancel_timer({tref, 0}),
  exit({{{{mocking_error, {unexpected, fuse_time:cancel_timer({tref, 0})}},
          [{eqc_mocking, f6092900_0,
              [fuse_time, cancel_timer, [{tref, 0}]],
              [{file, "../../eqc-project/src/eqc_mocking.erl"}, {line, 398}]},
           {eqc_mocking, do_action, 3,
              [{file, "../../eqc-project/src/eqc_mocking.erl"}, {line, 394}]},
           {fuse_server, reset_timer, 1,
              [{file, "src/fuse_server.erl"}, {line, 352}]},
           {fuse_server, handle_call, 3,
              [{file, "src/fuse_server.erl"}, {line, 173}]},
           {gen_server, try_handle_call, 4,
              [{file, "gen_server.erl"}, {line, 615}]},
           {gen_server, handle_msg, 5,
              [{file, "gen_server.erl"}, {line, 647}]},
           {proc_lib, init_p_do_apply, 3,
              [{file, "proc_lib.erl"}, {line, 247}]}]},
         {gen_server, call,
            [fuse_server,
             {install,
                {fuse, phineas, 1, 1, 1, [], {gradual, 1.0e-19}, none,
                   true}}]}},
        [{gen_server, call, 2, [{file, "gen_server.erl"}, {line, 204}]},
         {fuse_eqc, install, 2,
            [{file, "test/fuse_eqc.erl"}, {line, 166}]},
         {eqc_cluster_callbacks, wrap_call, 3,
            [{file, "../../eqc-project/src/eqc_cluster_callbacks.erl"},
             {line, 543}]}]}).

S: [{fuse_time_eqc,
       {state, 0, [{1, 0, '_', {reset, phineas}}], 1}},
    {fuse_eqc,
       {state, [],
          [{phineas,
              {fuse, {fault_injection, 1.0e-19}, 1, 1, ok, undefined,
                 [{delay, 1}], false}}]}}]


Reason:
  Post-condition failed:
  Exception:
    {{{{mocking_error, {unexpected, fuse_time:cancel_timer({tref, 0})}},
       [{eqc_mocking, f6092900_0,
           [fuse_time, cancel_timer, [{tref, 0}]],
           [{file, "../../eqc-project/src/eqc_mocking.erl"}, {line, 398}]},
        {eqc_mocking, do_action, 3,
           [{file, "../../eqc-project/src/eqc_mocking.erl"}, {line, 394}]},
        {fuse_server, reset_timer, 1,
           [{file, "src/fuse_server.erl"}, {line, 352}]},
        {fuse_server, handle_call, 3,
           [{file, "src/fuse_server.erl"}, {line, 173}]},
        {gen_server, try_handle_call, 4,
           [{file, "gen_server.erl"}, {line, 615}]},
        {gen_server, handle_msg, 5,
           [{file, "gen_server.erl"}, {line, 647}]},
        {proc_lib, init_p_do_apply, 3,
           [{file, "proc_lib.erl"}, {line, 247}]}]},
      {gen_server, call,
         [fuse_server,
          {install,
             {fuse, phineas, 1, 1, 1, [], {gradual, 1.0e-19}, none, true}}]}},
     [{gen_server, call, 2, [{file, "gen_server.erl"}, {line, 204}]},
      {fuse_eqc, install, 2,
         [{file, "test/fuse_eqc.erl"}, {line, 166}]},
      {eqc_cluster_callbacks, wrap_call, 3,
         [{file, "../../eqc-project/src/eqc_cluster_callbacks.erl"},
          {line, 543}]}]}
  Callout mismatch: unexpected: fuse_time:cancel_timer({tref, 0})
false
20>
@jlouis
Copy link
Owner Author

jlouis commented Sep 2, 2016

The bug happens due to the following circumstances:

  • Install a fuse
  • Melt it until it blows
  • Re-install the fuse.

The problem is:

  • The model doesn't cancel the timer when re-installing thought it should do that.

@jlouis
Copy link
Owner Author

jlouis commented Sep 2, 2016

Thought: The timer models can be simplified quite a lot here, if we thing about what we are trying to do. A good description of when the timers fail and what they do will help in the future by factoring the timer cancels correctly.

@jlouis
Copy link
Owner Author

jlouis commented Sep 2, 2016

Goal: figure out the invariants. If we know these, we can answer side-questions easily.

@jlouis jlouis closed this as completed Sep 2, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@jlouis