Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

i#5784: Fix false positives in invariant checker #5788

Merged
merged 4 commits into from
Dec 15, 2022
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 32 additions & 0 deletions clients/drcachesim/tests/invariant_checker_test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -246,6 +246,38 @@ check_kernel_xfer()
if (!run_checker(memrefs, false))
return false;
}
// Signal before any instr in the trace.
{
std::vector<memref_t> memrefs = {
// No instr in the beginning here.
gen_marker(1, TRACE_MARKER_TYPE_KERNEL_EVENT, 2),
gen_instr(1, 101),
// XXX: This marker value is actually not guaranteed, yet the checker
// requires it and the view tool prints it.
gen_marker(1, TRACE_MARKER_TYPE_KERNEL_XFER, 102),
gen_instr(1, 2),
};
if (!run_checker(memrefs, false))
return false;
}
// Nested signals without any intervening instr.
abhinav92003 marked this conversation as resolved.
Show resolved Hide resolved
{
std::vector<memref_t> memrefs = {
gen_instr(1, 1),
gen_marker(1, TRACE_MARKER_TYPE_KERNEL_EVENT, 2),
// No intervening instr here.
gen_marker(1, TRACE_MARKER_TYPE_KERNEL_EVENT, 101),
gen_instr(1, 201),
// XXX: This marker value is actually not guaranteed, yet the checker
// requires it and the view tool prints it.
abhinav92003 marked this conversation as resolved.
Show resolved Hide resolved
gen_marker(1, TRACE_MARKER_TYPE_KERNEL_XFER, 202),
gen_instr(1, 101),
gen_marker(1, TRACE_MARKER_TYPE_KERNEL_XFER, 102),
gen_instr(1, 2),
};
if (!run_checker(memrefs, false))
return false;
}
// Fail to return to recorded interruption point.
{
std::vector<memref_t> memrefs = {
Expand Down
39 changes: 27 additions & 12 deletions clients/drcachesim/tools/invariant_checker.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -414,16 +414,19 @@ invariant_checker_t::parallel_shard_memref(void *shard_data, const memref_t &mem
// resumption point.
shard->pre_signal_instr_.top().instr.type ==
TRACE_TYPE_INSTR_SYSENTER) &&
(memref.instr.addr == shard->pre_signal_instr_.top().instr.addr ||
// Asynch will go to the subsequent instr.
memref.instr.addr ==
shard->pre_signal_instr_.top().instr.addr +
shard->pre_signal_instr_.top().instr.size ||
// Too hard to figure out branch targets. We have the
// prev_xfer_int_pc_ though.
type_is_instr_branch(shard->pre_signal_instr_.top().instr.type) ||
shard->pre_signal_instr_.top().instr.type ==
TRACE_TYPE_INSTR_SYSENTER)) ||
(
// Skip pre_signal_instr_ check if there was no such instr.
shard->pre_signal_instr_.top().instr.addr == 0 ||
memref.instr.addr == shard->pre_signal_instr_.top().instr.addr ||
// Asynch will go to the subsequent instr.
memref.instr.addr ==
shard->pre_signal_instr_.top().instr.addr +
shard->pre_signal_instr_.top().instr.size ||
// Too hard to figure out branch targets. We have the
// prev_xfer_int_pc_ though.
type_is_instr_branch(shard->pre_signal_instr_.top().instr.type) ||
shard->pre_signal_instr_.top().instr.type ==
TRACE_TYPE_INSTR_SYSENTER)) ||
// Nested signal. XXX: This only works for our annotated test
// signal_invariants where we know shard->app_handler_pc_.
memref.instr.addr == shard->app_handler_pc_ ||
Expand All @@ -438,6 +441,7 @@ invariant_checker_t::parallel_shard_memref(void *shard_data, const memref_t &mem
}
#endif
shard->prev_instr_ = memref;
shard->saw_kernel_xfer_after_prev_instr_ = false;
// Clear prev_xfer_marker_ on an instr (not a memref which could come between an
// instr and a kernel-mediated far-away instr) to ensure it's *immediately*
// prior (i#3937).
Expand Down Expand Up @@ -483,8 +487,19 @@ invariant_checker_t::parallel_shard_memref(void *shard_data, const memref_t &mem
"Kernel event marker value missing");
if (memref.marker.marker_type == TRACE_MARKER_TYPE_KERNEL_EVENT &&
// Give up on back-to-back signals.
abhinav92003 marked this conversation as resolved.
Show resolved Hide resolved
abhinav92003 marked this conversation as resolved.
Show resolved Hide resolved
shard->prev_xfer_marker_.marker.marker_type != TRACE_MARKER_TYPE_KERNEL_XFER)
shard->pre_signal_instr_.push(shard->prev_instr_);
shard->prev_xfer_marker_.marker.marker_type !=
TRACE_MARKER_TYPE_KERNEL_XFER) {
if (shard->saw_kernel_xfer_after_prev_instr_) {
// We have nested signals without an intervening app instr.
// Push an empty instr to mean that this shouldn't be used.
shard->pre_signal_instr_.push({});
} else {
shard->saw_kernel_xfer_after_prev_instr_ = true;
// If there was a kernel xfer marker at the very beginning
// of the trace, we may still push an empty instr here.
shard->pre_signal_instr_.push(shard->prev_instr_);
}
}
#endif
shard->prev_xfer_marker_ = memref;
shard->last_xfer_marker_ = memref;
Expand Down
1 change: 1 addition & 0 deletions clients/drcachesim/tools/invariant_checker.h
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,7 @@ class invariant_checker_t : public analysis_tool_t {
int instrs_until_interrupt_ = -1;
int memrefs_until_interrupt_ = -1;
#endif
bool saw_kernel_xfer_after_prev_instr_ = false;
bool saw_timestamp_but_no_instr_ = false;
bool found_cache_line_size_marker_ = false;
bool found_instr_count_marker_ = false;
Expand Down