diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 3980db5..e9e0869 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -17,6 +17,7 @@ # import os, re, sys, signal, platform, click +import time if os.name == "posix": import resource, fcntl import subprocess @@ -98,6 +99,7 @@ class SbyProc: self.silent = silent self.wait = False self.job_lease = None + self.next_db = 0.0 self.task.update_proc_pending(self) @@ -183,6 +185,29 @@ class SbyProc: self.task.cancel() return + if time.time() >= self.next_db: + tasks_status = self.task.status_db.all_tasks_status() + for task_status in tasks_status.values(): + if (task_status["status"] in ["PASS", "FAIL", "CANCELLED"] and + task_status["name"] in self.task.cancelledby): + if not self.silent: + status_time = time.localtime(task_status["status_created"]) + if status_time.tm_yday == time.localtime().tm_yday: + # same day, format time only + time_format = r"%H:%M:%S" + else: + time_format = r"%x %H:%M:%S" + self.task.log( + f'Cancelled by {task_status["name"]!r} task ' + f'with status {task_status["status"]!r} ' + f'at {time.strftime(time_format, status_time)} ' + '(consider calling sby with --statusreset if this seems wrong)' + ) + self.task.cancel() + return + # don't hit the database every poll + self.next_db = time.time() + 10 + if not self.running: for dep in self.deps: if not dep.finished: @@ -226,6 +251,10 @@ class SbyProc: if self.job_lease: self.job_lease.done() + if self.terminated: + # task already terminated, do not finish + return + if not self.silent: self.task.log(f"{click.style(self.info, fg='magenta')}: finished (returncode={self.p.returncode})") diff --git a/sbysrc/sby_status.py b/sbysrc/sby_status.py index e0aca1f..78df944 100644 --- a/sbysrc/sby_status.py +++ b/sbysrc/sby_status.py @@ -295,6 +295,18 @@ class SbyStatusDb: return {row["id"]: dict(row) for row in rows} + def all_tasks_status(self): + rows = self.db.execute( + """ + SELECT task.id, task.name, task.created, + task_status.status, task_status.created as 'status_created' + FROM task + INNER JOIN task_status ON task_status.task=task.id + """ + ).fetchall() + + return {row["id"]: dict(row) for row in rows} + def all_task_properties(self): rows = self.db.execute( """ diff --git a/tests/intertask/Makefile b/tests/intertask/Makefile new file mode 100644 index 0000000..dc674bb --- /dev/null +++ b/tests/intertask/Makefile @@ -0,0 +1,2 @@ +SUBDIR=intertask +include ../make/subdir.mk diff --git a/tests/intertask/killer.sby b/tests/intertask/cancelledby.sby similarity index 74% rename from tests/intertask/killer.sby rename to tests/intertask/cancelledby.sby index 8092c8c..6163874 100644 --- a/tests/intertask/killer.sby +++ b/tests/intertask/cancelledby.sby @@ -10,28 +10,28 @@ c: a [options] mode bmc -depth 100 +depth 10000 expect fail,cancelled [engines] btor btormc [script] -a: read -define MAX=7 -b: read -define MAX=14 -c: read -define MAX=3 +a: read -define MAX=9600 +b: read -define MAX=1267 +c: read -define MAX=7200 read -formal demo.sv prep -top demo [file demo.sv] module demo ( input clk, - output reg [5:0] counter + output reg [31:0] counter ); initial counter = 0; always @(posedge clk) begin - if (counter == 15) + if (counter[31] == 1'b1) counter <= 0; else counter <= counter + 1;