Untrustworthy outputs of multi-threaded verifications

[zjp-CN]

The output log of verify-rust-std is untrustworthy in multi-threaded verifications.

# Copied from the CI, run with 16 threads (-j)
scripts/run-kani.sh --run autoharness --kani-args \
  --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \
  --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::unchecked_disjoint_bitor" \
  --include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::backward_unchecked" \
  --include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::forward_unchecked" \
  --include-pattern alloc::__default_lib_allocator:: \
  --include-pattern alloc::layout::Layout::from_size_align \
  --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
  --include-pattern char::convert::from_u32_unchecked \
  --include-pattern core_arch::x86::__m128d::as_f64x2 \
  --include-pattern "convert::num::<impl.convert::From<num::nonzero::NonZero<" \
  --include-pattern "num::<impl.i8>::unchecked_add" \
  --include-pattern "num::<impl.i16>::unchecked_add" \
  --include-pattern "num::<impl.i32>::unchecked_add" \
  --include-pattern "num::<impl.i64>::unchecked_add" \
  --include-pattern "num::<impl.i128>::unchecked_add" \
  --include-pattern "num::<impl.isize>::unchecked_add" \
  --include-pattern "num::<impl.u8>::unchecked_add" \
  --include-pattern "num::<impl.u16>::unchecked_add" \
  --include-pattern "num::<impl.u32>::unchecked_add" \
  --include-pattern "num::<impl.u64>::unchecked_add" \
  --include-pattern "num::<impl.u128>::unchecked_add" \
  --include-pattern "num::<impl.usize>::unchecked_add" \
  --include-pattern "num::<impl.i8>::unchecked_neg" \
  --include-pattern "num::<impl.i16>::unchecked_neg" \
  --include-pattern "num::<impl.i32>::unchecked_neg" \
  --include-pattern "num::<impl.i64>::unchecked_neg" \
  --include-pattern "num::<impl.i128>::unchecked_neg" \
  --include-pattern "num::<impl.isize>::unchecked_neg" \
  --include-pattern "num::<impl.i8>::unchecked_sh" \
  --include-pattern "num::<impl.i16>::unchecked_sh" \
  --include-pattern "num::<impl.i32>::unchecked_sh" \
  --include-pattern "num::<impl.i64>::unchecked_sh" \
  --include-pattern "num::<impl.i128>::unchecked_sh" \
  --include-pattern "num::<impl.isize>::unchecked_sh" \
  --include-pattern "num::<impl.u8>::unchecked_sh" \
  --include-pattern "num::<impl.u16>::unchecked_sh" \
  --include-pattern "num::<impl.u32>::unchecked_sh" \
  --include-pattern "num::<impl.u64>::unchecked_sh" \
  --include-pattern "num::<impl.u128>::unchecked_sh" \
  --include-pattern "num::<impl.usize>::unchecked_sh" \
  --include-pattern "num::<impl.i8>::unchecked_sub" \
    --include-pattern "num::<impl.i16>::wrapping_sh" \
    --include-pattern "num::<impl.i32>::wrapping_sh" \
    --include-pattern "num::<impl.i64>::wrapping_sh" \
    --include-pattern "num::<impl.i128>::wrapping_sh" \
    --include-pattern "num::<impl.isize>::wrapping_sh" \
    --include-pattern "num::<impl.u8>::wrapping_sh" \
    --include-pattern "num::<impl.u16>::wrapping_sh" \
    --include-pattern "num::<impl.u32>::wrapping_sh" \
    --include-pattern "num::<impl.u64>::wrapping_sh" \
    --include-pattern "num::<impl.u128>::wrapping_sh" \
    --include-pattern "num::<impl.usize>::wrapping_sh" \
    --include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<i64>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<i128>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<isize>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<u8>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<u16>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<u32>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<u64>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<u128>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<usize>::count_ones" \
    --include-pattern "num::nonzero::NonZero::<i8>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<i16>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<i32>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<i64>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<i128>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<isize>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<u8>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<u16>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<u32>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<u64>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<u128>::rotate_" \
    --include-pattern "num::nonzero::NonZero::<usize>::rotate_" \
    --include-pattern ptr::align_offset::mod_inv \
    --include-pattern ptr::alignment::Alignment::as_nonzero \
    --include-pattern ptr::alignment::Alignment::as_usize \
    --include-pattern ptr::alignment::Alignment::log2 \
    --include-pattern ptr::alignment::Alignment::mask \
    --include-pattern ptr::alignment::Alignment::new \
    --include-pattern ptr::alignment::Alignment::new_unchecked \
    --include-pattern time::Duration::from_micros \
    --include-pattern time::Duration::from_millis \
    --include-pattern time::Duration::from_nanos \
    --exclude-pattern time::Duration::from_nanos_u128 \
    --include-pattern time::Duration::from_secs \
    --exclude-pattern time::Duration::from_secs_f \
    --include-pattern unicode::unicode_data::conversions::to_ \
    --exclude-pattern ::precondition_check \
    --harness-timeout 10m \
    --default-unwind 1000 \
    -j --output-format=terse | tee autoharness-verification.log

with Kani version: at 54bb431831f9 as verify-rust-std currently requires

I expected to see this happen: the start and end (status) of single verification should be displayed continuously without interleaving

Instead, this happened: outputs of verifications from other threads may interleave 👇

Thread 14: Checking harness slice::iter::verify::verify_unit::check_count...
Thread 20: Checking harness slice::iter::verify::verify_u8::check_as_slice...
Thread 11: Checking harness slice::iter::verify::verify_char::check_len...
Thread 27: Checking harness str::validations::verify::check_run_utf8_validation...
Thread 14:
VERIFICATION RESULT:
 ** 0 of 96 failed (6 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 1.4218583s

Thread 20:
VERIFICATION RESULT:
 ** 0 of 202 failed (2 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 1.4005461s

Thread 0:
VERIFICATION RESULT:
 ** 0 of 544 failed (9 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 11.00833s

[zhassan-aws]

Thanks @zjp-CN for filing this issue. To avoid the confusion with interleaved output, our intention was to prefix each printed line with the thread index, but looks like we're missing some lines.

[tautschnig]

My workaround for this issue was to implement https://github.com/model-checking/verify-rust-std/blob/main/scripts/kani-std-analysis/log_parser.py; arguably that Python tool also does some more work, but a key piece is parse_log_lines (https://github.com/model-checking/verify-rust-std/blob/main/scripts/kani-std-analysis/log_parser.py#L428).