mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-15 17:33:38 +00:00
Estimated hours taken: 8
Branches: main
Rationalize the mechanisms we use to control retry across I/O.
After this change, we never ask questions about retry across I/O if the retry
is guaranteed to be safe. If the I/O is not guaranteed to be safe, there are
three things we can do:
- We ask the user whether they really want to. This is the default, and can be
asked for explicitly with "retry --interactive".
- We perform the retry without asking questions. This can be asked for
explicitly with "retry --force".
- We abort the retry automatically without asking questions. This can be asked
for explicitly with "retry --only-if-safe".
The implicit retries used to implement declarative debugging and the indirect
retries needed in the presence of minimal model tabling use the last option.
We need two conditions for the retry to be guaranteed to be safe:
- All I/O actions must be tabled.
- The retry must be wholly within the tabled region of the execution.
The first is normally assured by a debugging grade. However, to allow test
cases to test the behavior of retries even with --only-if-safe (and hence to
allow the testing of declarative debugging), we have another new flag,
--assume-all-io-is-tabled, which asserts the first condition to be true
even in non-debugging grades. This option applies both to the retry command
and the dd and dd_dd commands.
doc/user_guide.texi:
Move the misc commands (which are intended for use by everybody)
before the experimental and developer commands (which are intended
for use only by developers).
Document the dd_dd command in the developer section.
Document the new options of the retry, dd and dd_dd commands, with
the documentation of the developer-only options commented out.
Consolidate the documentation of the two variants of the retry command
into one, in order to reduce duplication.
Add a cross-reference requested by Fergus.
Add an XXX asking Mark to document the optional argument of dd_dd.
doc/generate_mdb_doc:
Switch the order of sections to match the change in user_guide.texi.
doc/mdb_categories:
Switch the order of sections to match the change in user_guide.texi,
and include dd and dd_dd in the command lists.
runtime/mercury_trace_base.[ch]:
Add a pair of global variables recording the event numbers at which
I/O tabling is turned on and off.
Make some declarations use the right typedef.
trace/mercury_trace.[ch]:
Make MR_trace_retry respect the values of the new options
controlling retries passed to it.
Convert this file to four-space indentation to reduce the number of
line-wraps.
trace/mercury_trace_declarative.[ch]:
Record the value of one of the options controlling retries for the
current invocation of `dd' in a global variable, since the front end
can initiate retries even after the initial retry.
Pass the required option values to retry.
trace/mercury_trace_external.c:
Pass the required option values to retry.
trace/mercury_trace_internal.c:
Implement the new options of the retry, dd and dd_dd commands.
Pass the required option values to retry.
Make "table_io start" and "table_io stop" record the relevant event
numbers in the global variables designed to hold them, for use in
mercury_trace.c in deciding whether a retry is safe.
Make indirect retries (used only in minimal model grades) use only safe
retries.
Make the dd and dd_dd commands use the help system to print usage
messages, now that they are both documented.
To make this possible, make the dd command part of the "misc" category
and the dd_dd command part of the "developer" category, which are the
categories they are documented under in user_guide.texi.
tests/debugger/mdb_command_test.inp:
Update this automatically generated list of commands.
tests/debugger/tabled_read.{inp,exp}:
tests/debugger/tabled_read_decl.{inp,exp}:
Update the retry commands in these tests to use the new options
where relevant.
tests/debugger/declarative/tabled_read_decl.{inp,exp}:
Update the dd commands in these tests to use the new options
where relevant.
23 lines
245 B
Plaintext
23 lines
245 B
Plaintext
echo on
|
|
register --quiet
|
|
context none
|
|
table_io allow
|
|
table_io
|
|
break tabled_read__test
|
|
table_io start
|
|
continue
|
|
finish -n
|
|
print *
|
|
retry -o -a
|
|
print *
|
|
finish -n
|
|
print *
|
|
table_io end
|
|
continue
|
|
finish -n
|
|
print *
|
|
retry -f
|
|
finish -n
|
|
print *
|
|
continue -S
|