fizzbee icon indicating copy to clipboard operation
fizzbee copied to clipboard

call statement causes crash state that triggers deadlock

Open tekumara opened this issue 1 year ago • 3 comments

Using a call statement causes a crash state to be generated that leads to a deadlock - should this happen?

Given:

---
action_options:
    Human.Input:
        max_actions: 2
        max_concurrent_actions: 1
---

role Human:

  action Input:
    input = None
    response = ui.history[-1] if ui.history else None
    if not response:
        input = ("Human","a")

    require input
    ui.input(input)
    pass    # ... more happens here ...

role ChatUI:
  action Init:
    self.history = []

  func input(input):
    self.history.append(input)
    pass    # ... more happens here ...

action Init:
  h = Human()
  ui = ChatUI()

I hit an unexpected deadlock because of a crash:

DEADLOCK detected
FAILED: Model checker failed
------
Init
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = []))"}
------
Human#0.Input
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = []))"}
------
thread-0
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = []))"}
------
thread-0
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = []))"}
------
thread-0
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = [(\"Human\", \"a\")]))"}
------
crash
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = [(\"Human\", \"a\")]))"}
------
Human#0.Input
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = [(\"Human\", \"a\")]))"}
------
crash
--
state: {"h":"role Human#0 (fields())","ui":"role ChatUI#0 (fields(history = [(\"Human\", \"a\")]))"}
------

I wasn't expecting this crash to cause a deadlock.

If however if I make the call statement a python statement, eg:

diff --git a/dl.fizz b/dl.fizz
index aa07973..2eeecbf 100644
--- a/dl.fizz
+++ b/dl.fizz
@@ -14,7 +14,7 @@ role Human:
         input = ("Human","a")
 
     require input
-    ui.input(input)
+    ui.history.append(input)
     pass    # ... more happens here ...
 
 role ChatUI:

The crash goes away and there are no deadlocks.

tekumara avatar Oct 19 '24 11:10 tekumara

action_options:
    Human.Input:
        max_actions: 2
        max_concurrent_actions: 1

Since it is set to a max of twice, this deadlock happens. Because it was called twice in the stack trace.

jp-fizzbee avatar Oct 29 '24 18:10 jp-fizzbee

Since it is set to a max of twice, this deadlock happens. Because it was called twice in the stack trace.

I thought with this change if max_actions is reached deadlock detection is skipped?

tekumara avatar Oct 30 '24 11:10 tekumara

Graph with the ui.input(input) call statement (note the crash state in the bottom right with no outgoing transition):

graph deadlocked

Vs the graph with ui.history.append(input) which doesn't deadlock - all states have an outgoing transition:

graph no deadlock

tekumara avatar Dec 01 '24 04:12 tekumara