diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 9fb3278..3f0a739 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -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 --------------- diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 0e966e7..e982fcc 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -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 diff --git a/sbysrc/sby_cmdline.py b/sbysrc/sby_cmdline.py index c94d9c2..cb2dedd 100644 --- a/sbysrc/sby_cmdline.py +++ b/sbysrc/sby_cmdline.py @@ -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") diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 7d37f93..93b7477 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) @@ -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: diff --git a/sbysrc/sby_status.py b/sbysrc/sby_status.py index e0aca1f..a8fc3a1 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 + 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}") 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/cancelledby.sby b/tests/intertask/cancelledby.sby new file mode 100644 index 0000000..e5771ab --- /dev/null +++ b/tests/intertask/cancelledby.sby @@ -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 diff --git a/tests/intertask/cancelledby.sh b/tests/intertask/cancelledby.sh new file mode 100644 index 0000000..940cacd --- /dev/null +++ b/tests/intertask/cancelledby.sh @@ -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 diff --git a/tests/intertask/longrunning.sby b/tests/intertask/longrunning.sby new file mode 100644 index 0000000..72cc44e --- /dev/null +++ b/tests/intertask/longrunning.sby @@ -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 diff --git a/tests/intertask/longrunning.sh b/tests/intertask/longrunning.sh new file mode 100644 index 0000000..3013897 --- /dev/null +++ b/tests/intertask/longrunning.sh @@ -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