mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-08-11 15:50:56 +00:00
Code Activity

Merge pull request #327 from YosysHQ/krys/intertask

Browse source 
Intertask cancellation
This commit is contained in:
KrystalDelusion 2025-07-09 10:48:21 +12:00 • committed by GitHub
commit ac120cee92
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 332 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

51
docs/source/reference.rst
View file

@ -202,6 +202,57 @@ options are:
| | | Values: ``on``, ``off``. Default: ``off`` |
+-------------------+------------+---------------------------------------------------------+
Cancelledby section
-------------------
At times it may be desirable for one task to be able to stop another task early,
such as when a ``prove`` task and a ``bmc`` task are testing the same properties
and the ``prove`` task finishes first, making the ``bmc`` task redundant. This
is where the optional ``[cancelledby]`` section comes in. Each line corresponds
to the name of a task which, if finished, will cancel the current task. No
distinction is made for whether the task finished successfully, only that
it is finished. Remember that tags can be used to control which tasks contain a
given configuration line.
Example:
.. code-block:: sby
[cancelledby]
task1:
task2
task3
task2:
task3
task4
In this example, ``task1`` can be cancelled by ``task2`` or ``task3``, while
``task2`` can be cancelled by ``task3`` or ``task4``. If ``task4`` is the first
to finish, then ``task2`` will be cancelled, which in turn leads to ``task1``
being cancelled. A task can only be cancelled if it has not yet finished, and
will check the finished tasks before starting and periodically while the
attached engines are running.
Normally, only the current taskloop is checked for finished tasks. This means
that intertask cancellations are not possible across separate SBY invocations or
when using the ``--sequential`` flag. By providing SBY with the
``--statuscancels`` flag however the status database will be used, allowing
tasks to be cancelled independently of taskloop. Note that this also means that
a task may be cancelled by a previous invocation unless ``--statusreset`` is
called first.
Example:
.. code-block:: shell
sby $sbyfile --statusreset
sby $sbyfile a b &
sby $sbyfile c d --statuscancels
In this example, the ``a`` and ``b`` tasks can only be cancelled by each other,
while the ``c`` and ``d`` tasks can be cancelled by any task.
Engines section
---------------

12
sbysrc/sby.py
View file

@ -62,6 +62,8 @@ jobcount = args.jobcount
init_config_file = args.init_config_file
status_show = args.status
status_reset = args.status_reset
status_cancels = args.status_cancels
task_status = args.task_status
status_live_csv = args.livecsv
status_show_csv = args.statuscsv
status_latest = args.status_latest
@ -70,7 +72,7 @@ if autotune and linkmode:
print("ERROR: --link flag currently not available with --autotune")
sys.exit(1)
if status_show or status_reset or status_show_csv:
if status_show or status_reset or task_status or status_show_csv:
target = workdir_prefix or workdir or sbyfile
if target is None:
print("ERROR: Specify a .sby config file or working directory to use --status.")
@ -96,7 +98,7 @@ if status_show or status_reset or status_show_csv:
if status_reset:
status_db.reset()
elif status_db.test_schema():
print(f"ERROR: Status database does not match expected formatted. Use --statusreset to reset.")
print(f"ERROR: Status database does not match expected format. Use --statusreset to reset.")
sys.exit(1)
if status_show:
@ -104,6 +106,9 @@ if status_show or status_reset or status_show_csv:
if status_show_csv:
status_db.print_status_summary_csv(tasknames, status_latest)
if task_status:
status_db.print_task_summary()
status_db.db.close()
@ -388,6 +393,7 @@ if dump_taskinfo:
"mode": cfg.options.get("mode"),
"engines": cfg.engines,
"script": cfg.script,
"cancelledby": cfg.cancelledby,
}
print(json.dumps(taskinfo, indent=2))
sys.exit(0)
@ -490,7 +496,7 @@ def start_task(taskloop, taskname):
else:
junit_filename = "junit"
task = SbyTask(sbyconfig, my_workdir, early_logmsgs, reusedir, taskloop, name=taskname, live_csv=status_live_csv)
task = SbyTask(sbyconfig, my_workdir, early_logmsgs, reusedir, status_cancels, taskloop, name=taskname, live_csv=status_live_csv)
for k, v in exe_paths.items():
task.exe_paths[k] = v

5
sbysrc/sby_cmdline.py
View file

@ -83,6 +83,11 @@ def parser_func(release_version='unknown SBY version'):
help="only check statuses from the most recent run of a task")
parser.add_argument("--statusreset", action="store_true", dest="status_reset",
help="reset the contents of the status database")
parser.add_argument("--statuscancels", action="store_true", dest="status_cancels",
help="intertask cancellations can be triggered by the status database")
parser.add_argument("--taskstatus", action="store_true", dest="task_status",
help="display the status of tasks in the status database")
parser.add_argument("--init-config-file", dest="init_config_file",
help="create a default .sby config file")

78
sbysrc/sby_core.py
View file

@ -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)
@ -149,8 +151,8 @@ class SbyProc:
if self.error_callback is not None:
self.error_callback(retcode)
def terminate(self, timeout=False):
if (self.task.opt_wait or self.wait) and not timeout:
def terminate(self, force=False):
if (self.task.opt_wait or self.wait) and not force:
return
if self.running:
if not self.silent:
@ -176,6 +178,36 @@ class SbyProc:
if self.finished or self.terminated or self.exited:
return
for task in self.task.taskloop.tasks_done:
if task.name in self.task.cancelledby:
if not self.silent:
self.task.log(f"Cancelled by {task.name!r} task")
self.task.cancel()
return
if self.task.status_cancels and 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:
@ -219,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})")
@ -283,6 +319,7 @@ class SbyConfig:
self.autotune_config = None
self.files = dict()
self.verbatim_files = dict()
self.cancelledby = list()
pass
def parse_config(self, f):
@ -403,6 +440,12 @@ class SbyConfig:
import sby_autotune
self.autotune_config = sby_autotune.SbyAutotuneConfig()
continue
if section == "cancelledby":
mode = "cancelledby"
if args is not None:
self.error(f"sby file syntax error: '[cancelledby]' section does not accept any arguments. got {args}")
continue
if section == "file":
mode = "file"
@ -437,6 +480,12 @@ class SbyConfig:
if mode == "autotune":
self.autotune_config.config_line(self, line)
continue
if mode == "cancelledby":
taskname = line.strip()
if taskname:
self.cancelledby.append(taskname)
continue
if mode == "engines":
args = line.strip().split()
@ -554,6 +603,7 @@ class SbyTaskloop:
self.procs_pending = []
self.procs_running = []
self.tasks = []
self.tasks_done = []
self.poll_now = False
self.jobclient = jobclient
@ -606,6 +656,7 @@ class SbyTaskloop:
self.tasks.append(task)
else:
task.exit_callback()
self.tasks_done.append(task)
for task in self.tasks:
task.exit_callback()
@ -862,12 +913,13 @@ class SbySummary:
class SbyTask(SbyConfig):
def __init__(self, sbyconfig, workdir, early_logs, reusedir, taskloop=None, logfile=None, name=None, live_csv=False):
def __init__(self, sbyconfig, workdir, early_logs, reusedir, status_cancels=False, taskloop=None, logfile=None, name=None, live_csv=False):
super().__init__()
self.used_options = set()
self.models = dict()
self.workdir = workdir
self.reusedir = reusedir
self.status_cancels = status_cancels
self.name = name
self.live_csv = live_csv
self.status = "UNKNOWN"
@ -1254,15 +1306,19 @@ class SbyTask(SbyConfig):
self.models[model_name] = self.make_model(model_name)
return self.models[model_name]
def terminate(self, timeout=False):
def terminate(self, timeout=False, cancel=False):
if timeout:
self.timeout_reached = True
for proc in list(self.procs_running):
proc.terminate(timeout=timeout)
proc.terminate(timeout or cancel)
for proc in list(self.procs_pending):
proc.terminate(timeout=timeout)
proc.terminate(timeout or cancel)
if timeout:
self.update_unknown_props(dict(source="timeout"))
def cancel(self):
self.terminate(cancel=True)
self.update_status("CANCELLED")
def proc_failed(self, proc):
# proc parameter used by autotune override
@ -1282,7 +1338,7 @@ class SbyTask(SbyConfig):
self.status_db.set_task_property_status(prop, data=data)
def update_status(self, new_status, step = None):
assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR", "CANCELLED"]
self.status_db.set_task_status(new_status)
if new_status == "UNKNOWN":
@ -1307,6 +1363,9 @@ class SbyTask(SbyConfig):
elif new_status == "ERROR":
self.status = "ERROR"
elif new_status == "CANCELLED":
self.status = "CANCELLED"
else:
assert 0
@ -1325,7 +1384,7 @@ class SbyTask(SbyConfig):
self.used_options.add("expect")
for s in self.expect:
if s not in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]:
if s not in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT", "CANCELLED"]:
self.error(f"Invalid expect value: {s}")
if self.opt_mode != "live":
@ -1465,7 +1524,7 @@ class SbyTask(SbyConfig):
else:
self.log("summary: " + click.style(line, fg="green" if self.status in self.expect else "red", bold=True))
assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]
assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT", "CANCELLED"]
if self.status in self.expect:
self.retcode = 0
@ -1475,6 +1534,7 @@ class SbyTask(SbyConfig):
if self.status == "UNKNOWN": self.retcode = 4
if self.status == "TIMEOUT": self.retcode = 8
if self.status == "ERROR": self.retcode = 16
if self.status == "CANCELLED": self.retcode = 32
def write_summary_file(self):
with open(f"{self.workdir}/{self.status}", "w") as f:

21
sbysrc/sby_status.py
View file

@ -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
LEFT 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(
"""
@ -387,6 +399,14 @@ class SbyStatusDb:
for display_name, statuses in sorted(properties.items()):
print(pretty_path(display_name), combine_statuses(statuses))
def print_task_summary(self):
tasks = self.all_tasks_status()
task_status = defaultdict(set)
for task in tasks.values():
task_status[task["name"]].add(task["status"] or "UNKNOWN")
for task_name, statuses in sorted(task_status.items()):
print(task_name, combine_statuses(statuses))
def get_status_data_joined(self, status_id: int):
row = self.db.execute(
"""
@ -567,5 +587,4 @@ def remove_db(path):
# no other connections, delete all tables
drop_script = cur.execute("SELECT name FROM sqlite_master WHERE type = 'table';").fetchall()
for table in drop_script:
print(table)
cur.execute(f"DROP TABLE {table}")

2
tests/intertask/Makefile Normal file
View file

@ -0,0 +1,2 @@
SUBDIR=intertask
include ../make/subdir.mk

47
tests/intertask/cancelledby.sby Normal file
View file

@ -0,0 +1,47 @@
[tasks]
c
b
a
[cancelledby]
a: b
b: c
c: a
[options]
mode bmc
depth 20
a: expect pass,cancelled
b: expect fail,cancelled
c: expect fail,cancelled
[engines]
btor btormc
[script]
a: read -define MAX=32
b: read -define MAX=12
c: read -define MAX=3
read -formal demo.sv
prep -top demo
[file demo.sv]
module demo (
input clk,
output reg [5:0] counter
);
initial counter = 0;
always @(posedge clk) begin
if (counter == 15)
counter <= 0;
else
counter <= counter + 1;
end
`ifdef FORMAL
always @(posedge clk) begin
assert (counter < `MAX);
end
`endif
endmodule

23
tests/intertask/cancelledby.sh Normal file
View file

@ -0,0 +1,23 @@
#!/bin/bash
set -e
if [[ $TASK == a ]]; then
# different process, no cancellations
rm -rf ${WORKDIR}_*
python3 $SBY_MAIN --prefix $WORKDIR $SBY_FILE a
python3 $SBY_MAIN --prefix $WORKDIR $SBY_FILE b
python3 $SBY_MAIN --prefix $WORKDIR $SBY_FILE c
test -e ${WORKDIR}_a/PASS -a -e ${WORKDIR}_b/FAIL -a -e ${WORKDIR}_c/FAIL
elif [[ $TASK == b ]]; then
# same process, a cancels c cancels b
# use statusdb so that the different taskloops from using --sequential doesn't matter
python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE a c b --sequential --statuscancels
test -e ${WORKDIR}_a/PASS -a -e ${WORKDIR}_b/CANCELLED -a -e ${WORKDIR}_c/CANCELLED
else
# different process, b cancels a, c completes before a
rm -rf ${WORKDIR} ${WORKDIR}_*
python3 $SBY_MAIN --prefix $WORKDIR $SBY_FILE b --statuscancels
python3 $SBY_MAIN --prefix $WORKDIR $SBY_FILE c --statuscancels
python3 $SBY_MAIN --prefix $WORKDIR $SBY_FILE a --statuscancels
echo test -e ${WORKDIR}_a/CANCELLED -a -e ${WORKDIR}_b/FAIL -a -e ${WORKDIR}_c/FAIL
fi

92
tests/intertask/longrunning.sby Normal file
View file

@ -0,0 +1,92 @@
[tasks]
bmc
prove
[cancelledby]
bmc: prove
[options]
bmc:
mode bmc
depth 20000
expect cancelled
prove:
mode prove
expect pass
--
[engines]
smtbmc boolector
[script]
read -sv autotune_div.sv
prep -top top
[file autotune_div.sv]
module top #(
parameter WIDTH = 4 // Reduce this if it takes too long on CI
) (
input clk,
input load,
input [WIDTH-1:0] a,
input [WIDTH-1:0] b,
output reg [WIDTH-1:0] q,
output reg [WIDTH-1:0] r,
output reg done
);
reg [WIDTH-1:0] a_reg = 0;
reg [WIDTH-1:0] b_reg = 1;
initial begin
q <= 0;
r <= 0;
done <= 1;
end
reg [WIDTH-1:0] q_step = 1;
reg [WIDTH-1:0] r_step = 1;
// This is not how you design a good divider circuit!
always @(posedge clk) begin
if (load) begin
a_reg <= a;
b_reg <= b;
q <= 0;
r <= a;
q_step <= 1;
r_step <= b;
done <= b == 0;
end else begin
if (r_step <= r) begin
q <= q + q_step;
r <= r - r_step;
if (!r_step[WIDTH-1]) begin
r_step <= r_step << 1;
q_step <= q_step << 1;
end
end else begin
if (!q_step[0]) begin
r_step <= r_step >> 1;
q_step <= q_step >> 1;
end else begin
done <= 1;
end
end
end
end
always @(posedge clk) begin
assert (r_step == b_reg * q_step); // Helper invariant
assert (q * b_reg + r == a_reg); // Main invariant & correct output relationship
if (done) assert (r <= b_reg - 1); // Output range
cover (done);
cover (done && b_reg == 0);
cover (r != a_reg);
cover (r == a_reg);
end
endmodule

14
tests/intertask/longrunning.sh Normal file
View file

@ -0,0 +1,14 @@
#!/bin/bash
set -e
if [[ $TASK == bmc ]]; then
python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE prove bmc
else
rm -rf ${WORKDIR} ${WORKDIR}_*
python3 $SBY_MAIN --prefix $WORKDIR $SBY_FILE bmc --statuscancels & bmc_pid="$!"
# make sure we don't leave the background task running
trap 'kill "$bmc_pid" 2>/dev/null || true' EXIT
python3 $SBY_MAIN --prefix $WORKDIR $SBY_FILE prove
sleep 10
test -e ${WORKDIR}_bmc/CANCELLED
fi