Skip to content

Conversation

@gc00
Copy link
Collaborator

@gc00 gc00 commented May 29, 2024

Probably, I will close this draft. The code is now in another PR.

Previously, the 'mcmini back' command in GDB mode was never really working.
This commit attempts to fix it.

@maxwellpirtle ,
There is a bug in mcmini_private.cpp, when I do mc_prepare_to_model_check_new_program(). I'm sure it's easy for you to fix this bug, or tell me how to do it.

I'm simply trying to re-initialize McMini to begin its search again at traceId==0. But as you can see from my suggested test, below, when I call mcmini back, instead of reducing the number of transitions for this trace from 9 to 8, instead, it grows the number of transitions. So, clearly I did not re-initialize McMini properly to again start at traceId==0. (For motivation, I'm trying to add support for mcmini back when interactively debugging a traceSeq, such as:

./mcmini-gdb -f -q -p 0 -p '0, 0, 0, 1, 1, 2' ./a.out

To test it, use your favorite target multithreaded application, a.out, and do:

./mcmini-gdb -q ../a.out
mcmini forward 9
mcmini printTransitions
mcmini back
mcmini printTransitions

@gc00 gc00 added the type: enhancement The issue specifies a feature that should be added to the project label May 29, 2024
@gc00 gc00 requested a review from maxwellpirtle May 29, 2024 19:23
@gc00 gc00 force-pushed the main branch 2 times, most recently from 8dabc7e to 813d1b6 Compare July 16, 2024 14:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

type: enhancement The issue specifies a feature that should be added to the project

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant