search

loonwerks / jkind

JKind - An infinite-state model checker for safety properties in Lustre
http://loonwerks.com/tools/jkind.html
Other
52 stars 32 forks source link

Abnormal termination exit code -8 during IVC reduction #76

Open kfhoech opened 5 months ago

kfhoech commented 5 months ago

The problem occurs where IVC reduction appears to be attempted on a property that has (possibly) been falsified.

image

These errors occur intermittently but on some models more consistently than on others. Running the same model multiple times the error might or might not occur. When the error does not occur, the property(ies) in question is(are) valid. When it does occur, the property(ies) is(are) unknown. It appears to be some sort of race condition.

Initial analysis indicates that the errors do rarely occur in Java VM version 1.8 but occur much more frequently in later JVM versions.

Application of the same Lustre file to multiple versions indicates the errors may occur in (at least) JKind versions 4.4.4, 4.5.0, and 4.5.2.

The it seems that setting pdr_max to zero either eliminates the bug or makes it so much less probably that it was not detected in a few dozen runs.

I am struggling to put together a simple model that illustrates the problem; changing anything appears to affect the likelihood of occurrence.

kfhoech commented 5 months ago

Here's a simple, sanitized example:

type Types__Human_Inputs__impl = struct {something_silly : real; pet_cat_select : Types__Play_Sleep_Eat; pet_dog_select : Types__Play_Sleep_Eat; pet_budgie_select : Types__Sleep_Eat; pet_hamster_select : Types__Play_Sleep_Eat};
type Types__Play_Sleep_Eat = enum {Types__Play_Sleep_Eat_Play, Types__Play_Sleep_Eat_Sleep, Types__Play_Sleep_Eat_Eat};
type Types__Sleep_Eat = enum {Types__Sleep_Eat_Sleep, Types__Sleep_Eat_Eat};
type Base_Types__Boolean = bool;
type Base_Types__Unsigned = int;
type Base_Types__Unsigned_64 = int;
type Base_Types__Unsigned_32 = int;
type Base_Types__Unsigned_16 = int;
type Base_Types__Unsigned_8 = int;
type Base_Types__Integer = int;
type Base_Types__Integer_64 = int;
type Base_Types__Integer_32 = int;
type Base_Types__Integer_16 = int;
type Base_Types__Integer_8 = int;
type Base_Types__Float = real;
type Base_Types__Float_32 = real;
type Base_Types__Float_64 = real;

node _TOP__demux(
  __ASSUME__HIST : bool;
  human_inputs : Types__Human_Inputs__impl;
  time : real;
  pet_cat_selection : Types__Play_Sleep_Eat;
  pet_dog_selection : Types__Play_Sleep_Eat;
  pet_budgie_selection : Types__Sleep_Eat;
  pet_hamster_selection : Types__Play_Sleep_Eat
) returns (
  __ASSERT : bool
);
var
  __GUARANTEE0 : bool;
  __GUARANTEE1 : bool;
  __GUARANTEE2 : bool;
  __GUARANTEE3 : bool;
let
  __GUARANTEE0 = (pet_cat_selection = human_inputs.pet_cat_select);

  __GUARANTEE1 = (pet_dog_selection = human_inputs.pet_dog_select);

  __GUARANTEE2 = (pet_budgie_selection = human_inputs.pet_budgie_select);

  __GUARANTEE3 = (pet_hamster_selection = human_inputs.pet_hamster_select);

  __ASSERT = (__ASSUME__HIST => (__GUARANTEE3 and (__GUARANTEE2 and (__GUARANTEE1 and __GUARANTEE0))));

  --%IVC __GUARANTEE0, __GUARANTEE1, __GUARANTEE2, __GUARANTEE3;

tel;

node _TOP__pet_select_switch_cat(
  __ASSUME__HIST : bool;
  human_input : Types__Play_Sleep_Eat;
  time : real;
  position : Types__Play_Sleep_Eat
) returns (
  __ASSERT : bool
);
var
  __GUARANTEE0 : bool;
let
  __GUARANTEE0 = (position = human_input);

  __ASSERT = (__ASSUME__HIST => __GUARANTEE0);

  --%IVC __GUARANTEE0;

tel;

node _TOP__pet_select_switch_dog(
  __ASSUME__HIST : bool;
  human_input : Types__Play_Sleep_Eat;
  time : real;
  position : Types__Play_Sleep_Eat
) returns (
  __ASSERT : bool
);
var
  __GUARANTEE0 : bool;
let
  __GUARANTEE0 = (position = human_input);

  __ASSERT = (__ASSUME__HIST => __GUARANTEE0);

  --%IVC __GUARANTEE0;

tel;

node _TOP__pet_select_switch_budgie(
  __ASSUME__HIST : bool;
  human_input : Types__Sleep_Eat;
  time : real;
  position : Types__Sleep_Eat
) returns (
  __ASSERT : bool
);
var
  __GUARANTEE0 : bool;
let
  __GUARANTEE0 = (position = human_input);

  __ASSERT = (__ASSUME__HIST => __GUARANTEE0);

  --%IVC __GUARANTEE0;

tel;

node _TOP__pet_select_switch_hamster(
  __ASSUME__HIST : bool;
  human_input : Types__Play_Sleep_Eat;
  time : real;
  position : Types__Play_Sleep_Eat
) returns (
  __ASSERT : bool
);
var
  __GUARANTEE0 : bool;
let
  __GUARANTEE0 = (position = human_input);

  __ASSERT = (__ASSUME__HIST => __GUARANTEE0);

  --%IVC __GUARANTEE0;

tel;

node main(
  demux__pet_cat_selection : Types__Play_Sleep_Eat;
  demux__pet_dog_selection : Types__Play_Sleep_Eat;
  demux__pet_budgie_selection : Types__Sleep_Eat;
  demux__pet_hamster_selection : Types__Play_Sleep_Eat;
  demux____ASSUME__HIST : bool;
  pet_select_switch_cat__position : Types__Play_Sleep_Eat;
  pet_select_switch_cat____ASSUME__HIST : bool;
  pet_select_switch_dog__position : Types__Play_Sleep_Eat;
  pet_select_switch_dog____ASSUME__HIST : bool;
  pet_select_switch_budgie__position : Types__Sleep_Eat;
  pet_select_switch_budgie____ASSUME__HIST : bool;
  pet_select_switch_hamster__position : Types__Play_Sleep_Eat;
  pet_select_switch_hamster____ASSUME__HIST : bool;
  pet_cat_selection : Types__Play_Sleep_Eat;
  pet_dog_selection : Types__Play_Sleep_Eat;
  pet_budgie_selection : Types__Sleep_Eat;
  pet_hamster_selection : Types__Play_Sleep_Eat;
  demux__human_inputs : Types__Human_Inputs__impl;
  demux__time : real;
  pet_select_switch_cat__human_input : Types__Play_Sleep_Eat;
  pet_select_switch_cat__time : real;
  pet_select_switch_dog__human_input : Types__Play_Sleep_Eat;
  pet_select_switch_dog__time : real;
  pet_select_switch_budgie__human_input : Types__Sleep_Eat;
  pet_select_switch_budgie__time : real;
  pet_select_switch_hamster__human_input : Types__Play_Sleep_Eat;
  pet_select_switch_hamster__time : real;
  human_inputs : Types__Human_Inputs__impl;
  time : real
) returns (

);
var
  __ASSUME__HIST : bool;
  __GUARANTEE0 : bool;
  __GUARANTEE1 : bool;
  __GUARANTEE2 : bool;
  __GUARANTEE3 : bool;
let
  --%MAIN;
  __ASSUME__HIST = (pet_select_switch_hamster____ASSUME__HIST and (pet_select_switch_budgie____ASSUME__HIST and (pet_select_switch_dog____ASSUME__HIST and (pet_select_switch_cat____ASSUME__HIST and (demux____ASSUME__HIST and true)))));

  __GUARANTEE0 = (pet_cat_selection = human_inputs.pet_cat_select);

  __GUARANTEE1 = (pet_dog_selection = human_inputs.pet_dog_select);

  __GUARANTEE2 = (pet_budgie_selection = human_inputs.pet_budgie_select);

  __GUARANTEE3 = (pet_hamster_selection = human_inputs.pet_hamster_select);

  assert (time = demux__time);

  assert _TOP__demux(demux____ASSUME__HIST, demux__human_inputs, demux__time, demux__pet_cat_selection, demux__pet_dog_selection, demux__pet_budgie_selection, demux__pet_hamster_selection);

  assert (demux____ASSUME__HIST = __HIST(true));

  assert (time = pet_select_switch_cat__time);

  assert _TOP__pet_select_switch_cat(pet_select_switch_cat____ASSUME__HIST, pet_select_switch_cat__human_input, pet_select_switch_cat__time, pet_select_switch_cat__position);

  assert (pet_select_switch_cat____ASSUME__HIST = __HIST(true));

  assert (time = pet_select_switch_dog__time);

  assert _TOP__pet_select_switch_dog(pet_select_switch_dog____ASSUME__HIST, pet_select_switch_dog__human_input, pet_select_switch_dog__time, pet_select_switch_dog__position);

  assert (pet_select_switch_dog____ASSUME__HIST = __HIST(true));

  assert (time = pet_select_switch_budgie__time);

  assert _TOP__pet_select_switch_budgie(pet_select_switch_budgie____ASSUME__HIST, pet_select_switch_budgie__human_input, pet_select_switch_budgie__time, pet_select_switch_budgie__position);

  assert (pet_select_switch_budgie____ASSUME__HIST = __HIST(true));

  assert (time = pet_select_switch_hamster__time);

  assert _TOP__pet_select_switch_hamster(pet_select_switch_hamster____ASSUME__HIST, pet_select_switch_hamster__human_input, pet_select_switch_hamster__time, pet_select_switch_hamster__position);

  assert (pet_select_switch_hamster____ASSUME__HIST = __HIST(true));

  assert (demux__pet_cat_selection = pet_select_switch_cat__human_input);

  assert (demux__pet_dog_selection = pet_select_switch_dog__human_input);

  assert (demux__pet_budgie_selection = pet_select_switch_budgie__human_input);

  assert (demux__pet_hamster_selection = pet_select_switch_hamster__human_input);

  assert (human_inputs = demux__human_inputs);

  assert (pet_select_switch_cat__position = pet_cat_selection);

  assert (pet_select_switch_dog__position = pet_dog_selection);

  assert (pet_select_switch_budgie__position = pet_budgie_selection);

  assert (pet_select_switch_hamster__position = pet_hamster_selection);

  assert true;

  assert (((time = 0.0) -> (time > (pre time))) and (true -> (time = ((pre time) + (time - (pre time))))));

  --%PROPERTY __ASSUME__HIST;
  --%PROPERTY __GUARANTEE0;
  --%PROPERTY __GUARANTEE1;
  --%PROPERTY __GUARANTEE2;
  --%PROPERTY __GUARANTEE3;

tel;

node __HIST(
  input : bool
) returns (
  hist : bool
);
let
  hist = (input -> ((pre hist) and input));

tel;

node __MinPos(
  a : real;
  b : real
) returns (
  ret : real
);
let
  ret = (if (a <= 0.0) then b else (if (b <= 0.0) then a else (if (a <= b) then a else b)));

tel;

node __Rise(
  input : bool
) returns (
  output : bool
);
let
  output = (input -> ((pre (not input)) and input));

tel;

node __Fall(
  input : bool
) returns (
  output : bool
);
let
  output = ((not input) -> ((pre input) and (not input)));

tel;

Command line used:

java -jar c:\jkind-4.5.2\jkind.jar -jkind -solver z3 -pdr_max 1 -ivc animals.lus

Output when error occurs:

==========================================
  JKind 4.5.2
==========================================

There are 5 properties to be checked.
PROPERTIES TO BE CHECKED: [__ASSUME__HIST, __GUARANTEE0, __GUARANTEE1, __GUARANTEE2, __GUARANTEE3]

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
VALID PROPERTIES: [__ASSUME__HIST] || pdr || K = 1 || Time = 0.343s
INVARIANTS:
  __ASSUME__HIST
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
UNKNOWN PROPERTIES: [__GUARANTEE0, __GUARANTEE1, __GUARANTEE2, __GUARANTEE3] || True for 44 steps || Time = 0.36s
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

    -------------------------------------
    --^^--        SUMMARY          --^^--
    -------------------------------------

VALID PROPERTIES: [__ASSUME__HIST]

UNKNOWN PROPERTIES: [__GUARANTEE0, __GUARANTEE1, __GUARANTEE2, __GUARANTEE3]

ivc-reduction process failed
jkind.JKindException: Trying to reduce IVC on falsifiable property
        at jkind.engines.ivcs.IvcReductionEngine.reduceIvc(IvcReductionEngine.java:160)
        at jkind.engines.ivcs.IvcReductionEngine.reduceInvariants(IvcReductionEngine.java:140)
        at jkind.engines.ivcs.IvcReductionEngine.reduce(IvcReductionEngine.java:69)
        at jkind.engines.ivcs.IvcReductionEngine.handleMessage(IvcReductionEngine.java:275)
        at jkind.engines.messages.ValidMessage.accept(ValidMessage.java:50)
        at jkind.engines.messages.MessageHandler.handleMessage(MessageHandler.java:42)
        at jkind.engines.messages.MessageHandler.processMessagesAndWaitUntil(MessageHandler.java:50)
        at jkind.engines.ivcs.IvcReductionEngine.main(IvcReductionEngine.java:62)
        at jkind.engines.Engine.run(Engine.java:36)
        at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
        at java.base/java.lang.Thread.run(Thread.java:829)

Output when error does not occur:

==========================================
  JKind 4.5.2
==========================================

There are 5 properties to be checked.
PROPERTIES TO BE CHECKED: [__ASSUME__HIST, __GUARANTEE0, __GUARANTEE1, __GUARANTEE2, __GUARANTEE3]

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
VALID PROPERTIES: [__ASSUME__HIST] || k-induction || K = 1 || Time = 0.334s
INVARIANTS:
  __ASSUME__HIST
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
VALID PROPERTIES: [__GUARANTEE0] || k-induction || K = 1 || Time = 0.349s
INVARIANTS:
  __ASSUME__HIST
  __GUARANTEE0
INDUCTIVE VALIDITY CORE:
  _TOP__demux~0.__GUARANTEE0
  _TOP__pet_select_switch_cat~0.__GUARANTEE0
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
VALID PROPERTIES: [__GUARANTEE1] || k-induction || K = 1 || Time = 0.36s
INVARIANTS:
  __ASSUME__HIST
  __GUARANTEE1
INDUCTIVE VALIDITY CORE:
  _TOP__demux~0.__GUARANTEE1
  _TOP__pet_select_switch_dog~0.__GUARANTEE0
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
VALID PROPERTIES: [__GUARANTEE2] || k-induction || K = 1 || Time = 0.369s
INVARIANTS:
  __ASSUME__HIST
  __GUARANTEE2
INDUCTIVE VALIDITY CORE:
  _TOP__demux~0.__GUARANTEE2
  _TOP__pet_select_switch_budgie~0.__GUARANTEE0
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
VALID PROPERTIES: [__GUARANTEE3] || k-induction || K = 1 || Time = 0.375s
INVARIANTS:
  __ASSUME__HIST
  __GUARANTEE3
INDUCTIVE VALIDITY CORE:
  _TOP__demux~0.__GUARANTEE3
  _TOP__pet_select_switch_hamster~0.__GUARANTEE0
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

    -------------------------------------
    --^^--        SUMMARY          --^^--
    -------------------------------------

VALID PROPERTIES: [__ASSUME__HIST, __GUARANTEE0, __GUARANTEE1, __GUARANTEE2, __GUARANTEE3]

PDR may be involved. Setting pdr_max to zero makes occurrence much more rare.

kfhoech commented 5 months ago

I originally thought this might be due to interactions to the solver in the parent class SolverBasedEngine not being synchronized. The theory was that thread A started an IVC reduction but was interrupted by thread B while adding assertions to the context. Then thread B pushes another assertion set into the solver which also does IVC reduction. But its interrupted by thread A again which adds the remainder of assertions, B resumes and makes the unsatQuery, pops an assertion set from the solver. But some of A's assertions were added after B pushing another assertion set and are thus missing from the query. However, adding synchronization to the methods in IvcReductionEngine that push or pop the solver stack don't seem to help. Investigation is ongoing.

kfhoech commented 5 months ago

This is pretty likely a race. Outputting scratch makes it much less likely to occur. It was difficult to capture a run where the error occurred. Attached are zipped collections of the scratch files. animals-bad.zip animals-good.zip