bblum/landslide

stateless model checking for thread libraries, kernels, and transactional memory

landslide's Issues

implement dpor sleep sets

on the test htm_fig61.c we explore a redundant interleaving in branch 7(ish), like:

T4, creation up to xbegin ~ T5, creation up to xbegin, (new branch part begins) T4 body of xbegin or whatever

this part of T5 was reordered up to where it was in the hopes of running T5's xbegin body or failure path or whatever before smth of T4. but to get there it first had to run an earlier transition of T5. then dpor was like, i wanna run T4 before this xbegin point, even though that just ends up equivalent to an interleaving already tested, it just ends up fruitlessly/inside-out-ly reordering the independent part of T5. possible ways of solving this:

• (good way) carry around a "sleep set" (i think) of like, memory conflicts that e.g. T5 did that justified it being reordered, and in the new branch, somehow make e.g. T5 unpreemptable until one of those memory accesses is performed.
• (maybe good way) look up what "optimal dpor" does (smth diff from above?) and do that
• (bad way) support explore backwards execution reordering with transactions (currently requires all txn branches explored first before exploring any other thread... i think?)

there's a piece of paper with scribblings on it, sitting right next to me now as i write this bug report, that details this but i tried to summarize in text too

bochs crash on setup on certain machines, not on others

========================================================================
                       Bochs x86 Emulator 2.6.8
                Built from SVN snapshot on May 3, 2015
                  Compiled on Dec 26 2018 at 02:14:54
========================================================================
00000000000p[      ] >>PANIC<< dlopen failed for module 'unmapped': file not found
========================================================================
Bochs is exiting with the following message:
[      ] dlopen failed for module 'unmapped': file not found
========================================================================

it's particularly nasty because it's before thunderbirds, so quicksand just hangs;

i looked into this a while ago and it had something to do with the build process. libtool perhaps, or another tool involved in the chain, was failing to generate compile targets for a bunch of the modules. it works on unix*.andrew and on my current checkouts on my laptop, but not on a fresh checkout on laptop, and not on office machine.

i couldn't figure out last time how to properly generate those compile targets. i don't remember now exactly what they were.

soundness problem with xbegin PPs

htm_soundness checks for this, containing an intentional bug that dpor will skip over

for example from the transition

T4 up to xbegin, T4 failure injection path*, T5 up to xbegin, T5 txnal path* (* conflict with each other)

the alternate interleaving was tagged to explore:

T4 up to xbegin, T5 (...presumably thereafter, T4 both txn and failure path interleavings)

however, when T4 is next switched back to after T5 (whether through preemption or through a voluntary reschedule), the new PP thereupon is not considered an "xbegin" PP and so the chance to failure inject on T4 is lost in this subtree. hence

T4 up to xbegin, T5 up to xbegin, T5 txnal path, T4 failure injection path

will not be testedことになっちゃうのである。

410user/inc/thread.h should not include thr_internals.h (at least for PSU)

the psu handout doesn't have this include, and if a studence puts for example "include thread.h" in their e.g. cond_type.h, that can cause a circular include cycle and break the build (even tho it would succeed in psu's basecode).

i tried just removing it but it makes libthrgrp fail to build (didn't quite figure out why), so maybe like psu doesn't even include

import-p2.sh should make clean after rsyncing

if you got a cross-machine import from a p2 directory where it has compiled objects built on another toolchain, the build in import-p2.sh will fail to link.

it should just make clean first...

"page fault" error message should be "seg fault" for p2s/psus

got a confused studence email about this so empirically it oughta be fixed

top level 'landslide' script check for exec2obj pointer fails to check substrings

if you type "./landslide -p fig63" for example, when there's no fig63 program but there is a htm_fig63, it will grep successfully for "fig63_exec2obj_userapp_code_ptr", and end up in the waiting-forever failure mode while the inner landslide instance fails to compile.

yield() loop unblocking detection needs to check for kernel scheduler runnability if loop cares about yield return value

The user_sync stuff detects if a yield loop should unblock by looking at conflicting memory accesses in the loop condition, assuming that it's checking some flag that another thread's gonna set. But, a yield loop can depend on the behaviour of another thread without any memory accesses simply by checking yield's return value -- when the target thread exits, yield returns -1. This technique is used by the rwlock_starve tests, for example.

This introduces unsoundness because the yield blocking thread will stay blocked long after the target thread exits, and depend on arbiter's false positive deadlock avoidance to kick it awake after all other threads have quiesced, instead of being woken up immediately.

I was not actually able to come up with a test case that would demonstrate this unsoundness, i.e., fail to find a bug that should be exposed if the thread were woken at the proper time. I think I tried for like an hour or so - trying to get a third thread to run some logic that would assert that it happened before the blocking thread got woken up, i.e., to assert that it quiesced as described above. I forget why I couldn't get it to work.

It may actually be that this is not unsound, and any behaviour that I was trying to hide in that third thread is also possible to expose in a different interleaving even under the current implementation. I'm not really sure, but in any event, Landslide should really be waking up yield-blocking threads whenever their yield target's runnability status changes (deschedule, exit; even make runnable, like a thread could loop until the rv stops being -1).

stack trace or read memory should check for cross page accesses and not blow up bochs if so

in your exit-UAF detailed bug study results file, the group marked with "issue #8" is the one that reproduces it

stack trace has a check for ebp = 0xFFFFFFFF, but that's not the only case that can cause bochs to blow up with "cross page read"

with physical address 0x1023fff (probably in stack trace but didn't confirm)

formalize quicksand's ability to ignore all the thread library functions as a cmdline option, like "don't test thrlib"

all the gross conditionals in job.c, they should be controllable via a cmdline flag

have quicksand print something better than "you survived" when maximal ss verified

in bug.c - found_any_bugs()

like, "No bugs found & maximal state space fully tested -- this test case is guaranteed bug-free!"

make quicksand detect compile errors by forking a separate program before any actual landslides, don't use message passing and get stuck like a big dummy