reappearing "ghost" key after 17 steps #50

Closed
cmumford opened this Issue Sep 9, 2014 · 8 comments

Comments

Projects
None yet
1 participant
@cmumford
Contributor

cmumford commented Sep 9, 2014

Original issue 44 created by josephwnorton on 2011-10-03T16:13:29.000Z:

I'm testing an Erlang-based API for leveldb via an Erlang NIF written in C++. The test model is written in Erlang with the help of the test tool QuickCheck. The test model and test tool have found a failing minimal test case of 17 steps that appears (but not proven yet) to be an issue with leveldb.

I tried to manually create a minimal failing example that in pure C++. Unfortunately, I am unable to reproduce the issue with a pure C++ test case.

I attached the failing counterexample case and leveldb data directory after closing of the database. I'm hoping the leveldb authors might be able to pinpoint the issue or provide some instructions on how to troubleshoot this issue.

What steps will reproduce the problem?

  1. open new database
  2. put key1 and val1
  3. close database
  4. open database
  5. delete key2
  6. delete key1
  7. close database
  8. open database
  9. delete key2
  10. close database
  11. open database
  12. put key3 and val1
  13. close database
  14. open database
  15. close database
  16. open database
  17. seek first

What is the expected output? key3 at step 17

What do you see instead? key1 at step 17

> foobar:test().

<<10,0,0,0,12>>/'$end_of_table': [{obj,6,0}]

'$end_of_table'/'$end_of_table': []

'$end_of_table'/'$end_of_table': []

<<18,193,216,96,0,8>>/'$end_of_table': [{obj,6,0}]

<<18,193,216,96,0,8>>/'$end_of_table': [{obj,6,0}]

<<10,0,0,0,12>>/<<18,193,216,96,0,8>>: [{obj,6,0},{obj,6,0}]
ok

What version of the product are you using? On what operating system?

commit 26db4d9
Author: Hans Wennborg <hans@chromium.org>
Date: Mon Sep 26 17:37:09 2011 +0100

The issue repeats on MacOS X Lion and Fedora 15.

Please provide any additional information below.

The following shutdown sequence is performed at the time of closing the database:

leveldb::WriteOptions db_write_options;
leveldb::WriteBatch batch;
leveldb::Status status;

db_write_options.sync = true;
status = h-&gt;db-&gt;Write(db_write_options, &amp;batch);
if (!status.ok()) {
    return MAKEBADARG(env, status);
}

delete h-&gt;db;
h-&gt;db = NULL;
@cmumford

This comment has been minimized.

Show comment
Hide comment
@cmumford

cmumford Sep 9, 2014

Contributor

Comment #1 originally posted by sanjay.ghemawat on 2011-10-03T18:30:02.000Z:

Do you have a C++ program that demonstrates the bug?

PS. Your erlang test ends with:
Key1 = lets_nif:impl_first(Tab6),
That seems to be checking that the result of step 17 is key1.
I presume you used to check
Key3 = ...
and this change to Key1 is just to make the test pass in the
presence of a bug in leveldb or your erlang wrapper? Or did
you just have a typo in the test and everything is actually
working correctly.

I tried emulating your program as a new test case in
leveldb/db/db_test.cc, and that test passed:

TEST(DBTest, ReopenMultipleTimes) {
std::string key1("\x0a\x00\x00\x00\x0c", 5);
std::string key2 = std::string("\x0a\x00\x00\x00\x01\x80", 6)
+ std::string(152, '2');
std::string key3("\x12\xc1\xd8\x60\x00\x08", 6);
std::string val = std::string("\x10\x00\x00\x00", 4) + std::string(17, '1');
ASSERT_OK(Put(key1, val));
Reopen();
ASSERT_OK(Delete(key2));
ASSERT_OK(Delete(key1));
Reopen();
ASSERT_OK(Delete(key2));
Reopen();
ASSERT_OK(Put(key3, val));
Reopen();
Reopen();
Iterator* iter = db_->NewIterator(ReadOptions());
iter->SeekToFirst();
ASSERT_EQ(key3, iter->key().ToString());
ASSERT_EQ(val, iter->value().ToString());
delete iter;
}

Contributor

cmumford commented Sep 9, 2014

Comment #1 originally posted by sanjay.ghemawat on 2011-10-03T18:30:02.000Z:

Do you have a C++ program that demonstrates the bug?

PS. Your erlang test ends with:
Key1 = lets_nif:impl_first(Tab6),
That seems to be checking that the result of step 17 is key1.
I presume you used to check
Key3 = ...
and this change to Key1 is just to make the test pass in the
presence of a bug in leveldb or your erlang wrapper? Or did
you just have a typo in the test and everything is actually
working correctly.

I tried emulating your program as a new test case in
leveldb/db/db_test.cc, and that test passed:

TEST(DBTest, ReopenMultipleTimes) {
std::string key1("\x0a\x00\x00\x00\x0c", 5);
std::string key2 = std::string("\x0a\x00\x00\x00\x01\x80", 6)
+ std::string(152, '2');
std::string key3("\x12\xc1\xd8\x60\x00\x08", 6);
std::string val = std::string("\x10\x00\x00\x00", 4) + std::string(17, '1');
ASSERT_OK(Put(key1, val));
Reopen();
ASSERT_OK(Delete(key2));
ASSERT_OK(Delete(key1));
Reopen();
ASSERT_OK(Delete(key2));
Reopen();
ASSERT_OK(Put(key3, val));
Reopen();
Reopen();
Iterator* iter = db_->NewIterator(ReadOptions());
iter->SeekToFirst();
ASSERT_EQ(key3, iter->key().ToString());
ASSERT_EQ(val, iter->value().ToString());
delete iter;
}

@cmumford

This comment has been minimized.

Show comment
Hide comment
@cmumford

cmumford Sep 9, 2014

Contributor

Comment #2 originally posted by josephwnorton on 2011-10-03T23:14:21.000Z:

Yes, I used key1 to make the test pass.

I created a C++ program by hand to repeat the issue but unfortunately I was unable to repeat the problem.

I need to spend more time to see how I can repeat the issue using only the c and/or c++ leveldb API.

Is there any debug or verbose mode that I can enable to trace the low level behavior of leveldb?

Contributor

cmumford commented Sep 9, 2014

Comment #2 originally posted by josephwnorton on 2011-10-03T23:14:21.000Z:

Yes, I used key1 to make the test pass.

I created a C++ program by hand to repeat the issue but unfortunately I was unable to repeat the problem.

I need to spend more time to see how I can repeat the issue using only the c and/or c++ leveldb API.

Is there any debug or verbose mode that I can enable to trace the low level behavior of leveldb?

@cmumford

This comment has been minimized.

Show comment
Hide comment
@cmumford

cmumford Sep 9, 2014

Contributor

Comment #3 originally posted by josephwnorton on 2011-10-26T15:02:42.000Z:

As a follow-up, the test used to find this bug has been uploaded to GitHub. There is also a simpler version that can repeat the behavior using leveldb's c bindings.

https://github.com/norton/lets/blob/master/test/qc/qc_statem_lets.erl
https://github.com/norton/lets/blob/leveldb-issue44/test/qc/qc_statemc_lets.erl

Contributor

cmumford commented Sep 9, 2014

Comment #3 originally posted by josephwnorton on 2011-10-26T15:02:42.000Z:

As a follow-up, the test used to find this bug has been uploaded to GitHub. There is also a simpler version that can repeat the behavior using leveldb's c bindings.

https://github.com/norton/lets/blob/master/test/qc/qc_statem_lets.erl
https://github.com/norton/lets/blob/leveldb-issue44/test/qc/qc_statemc_lets.erl

@cmumford

This comment has been minimized.

Show comment
Hide comment
@cmumford

cmumford Sep 9, 2014

Contributor

Comment #4 originally posted by josephwnorton on 2011-10-26T15:39:04.000Z:

The problem hasn't been fixed. I'm testing against the following version of leveldb. It is dated Oct 5 and not Oct 15. I was (mistakenly) waiting for the next release.

https://github.com/norton/leveldb/commits/master

commit 299cced
Author: Gabor Cselle gabor@google.com
Date: Wed Oct 5 16:30:28 2011 -0700

Contributor

cmumford commented Sep 9, 2014

Comment #4 originally posted by josephwnorton on 2011-10-26T15:39:04.000Z:

The problem hasn't been fixed. I'm testing against the following version of leveldb. It is dated Oct 5 and not Oct 15. I was (mistakenly) waiting for the next release.

https://github.com/norton/leveldb/commits/master

commit 299cced
Author: Gabor Cselle gabor@google.com
Date: Wed Oct 5 16:30:28 2011 -0700

@cmumford

This comment has been minimized.

Show comment
Hide comment
@cmumford

cmumford Sep 9, 2014

Contributor

Comment #5 originally posted by josephwnorton on 2011-10-29T12:02:28.000Z:

Sanjay -

I constructed a failing C test case to mimic the original QuickCheck Erlang counterexample. Please see the Makefile for details on how to build and to run.

https://github.com/norton/lets/blob/leveldb-issue44/priv/test/qc_leveldb_issue44.c

[(leveldb-issue44)]$ pwd
/lets/priv/test

[(leveldb-issue44)]$ make clean all; ./qc_leveldb_issue44
rm -rf *.o qc_leveldb
gcc -c -Wall -I ../../c_src/leveldb/include qc_statemc_lets.c -o qc_statemc_lets.o
gcc -c -Wall -I ../../c_src/leveldb/include qc_leveldb_issue44.c -o qc_leveldb_issue44.o
gcc qc_statemc_lets.o qc_leveldb_issue44.o ../../c_src/leveldb/lib/libleveldb.a ../../c_src/snappy/lib/libsnappy.a -lstdc++ -lpthread -o qc_leveldb_issue44

!!! NO - reappearing ghost key 'g' !!!

KEY POINT => sleep for background compaction to finish it's work

!!! YES - reappearing ghost key 'g' !!!

qc_leveldb_issue44: qc_leveldb_issue44.c:115: main: Assertion `buglen == nillen' failed.
Aborted

Contributor

cmumford commented Sep 9, 2014

Comment #5 originally posted by josephwnorton on 2011-10-29T12:02:28.000Z:

Sanjay -

I constructed a failing C test case to mimic the original QuickCheck Erlang counterexample. Please see the Makefile for details on how to build and to run.

https://github.com/norton/lets/blob/leveldb-issue44/priv/test/qc_leveldb_issue44.c

[(leveldb-issue44)]$ pwd
/lets/priv/test

[(leveldb-issue44)]$ make clean all; ./qc_leveldb_issue44
rm -rf *.o qc_leveldb
gcc -c -Wall -I ../../c_src/leveldb/include qc_statemc_lets.c -o qc_statemc_lets.o
gcc -c -Wall -I ../../c_src/leveldb/include qc_leveldb_issue44.c -o qc_leveldb_issue44.o
gcc qc_statemc_lets.o qc_leveldb_issue44.o ../../c_src/leveldb/lib/libleveldb.a ../../c_src/snappy/lib/libsnappy.a -lstdc++ -lpthread -o qc_leveldb_issue44

!!! NO - reappearing ghost key 'g' !!!

KEY POINT => sleep for background compaction to finish it's work

!!! YES - reappearing ghost key 'g' !!!

qc_leveldb_issue44: qc_leveldb_issue44.c:115: main: Assertion `buglen == nillen' failed.
Aborted

@cmumford

This comment has been minimized.

Show comment
Hide comment
@cmumford

cmumford Sep 9, 2014

Contributor

Comment #6 originally posted by josephwnorton on 2011-10-30T12:31:49.000Z:

Sanjay -

The previous patch did fix the previous issue. However, a new counterexample in 31 steps was found (and is repeatable). The failing post condition is same as previous issue - a reappearing ghost key.

[{init,{state,qc_statemc_lets,{state,false,false,undefined,[]}}},
{set,{var,1},{call,qc_leveldb,open,[]}},
{set,{var,3},{call,qc_leveldb,close,[{var,1}]}},
{set,{var,4},{call,qc_leveldb,reopen,[]}},
{set,{var,5},{call,qc_leveldb,put,[{var,4},{obj,<<>>,<<>>}]}},
{set,{var,7},{call,qc_leveldb,close,[{var,4}]}},
{set,{var,11},{call,qc_leveldb,reopen,[]}},
{set,{var,16},{call,qc_leveldb,delete,[{var,11},<<"~88I.1">>]}},
{set,{var,19},{call,qc_leveldb,put,[{var,11},{obj,<<>>,<<>>}]}},
{set,{var,25},{call,qc_leveldb,close,[{var,11}]}},
{set,{var,29},{call,qc_leveldb,reopen,[]}},
{set,{var,30},
{call,qc_leveldb,put,
[{var,29},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,127>>,
<<95,78,70,31,26>>}]}},
{set,{var,33},{call,qc_leveldb,close,[{var,29}]}},
{set,{var,34},{call,qc_leveldb,reopen,[]}},
{set,{var,35},{call,qc_leveldb,put,[{var,34},{obj,<<>>,<<>>}]}},
{set,{var,46},{call,qc_leveldb,close,[{var,34}]}},
{set,{var,47},{call,qc_leveldb,reopen,[]}},
{set,{var,49},{call,qc_leveldb,put,[{var,47},{obj,<<>>,<<>>}]}},
{set,{var,50},{call,qc_leveldb,close,[{var,47}]}},
{set,{var,51},{call,qc_leveldb,reopen,[]}},
{set,{var,52},{call,qc_leveldb,put,[{var,51},{obj,<<"l\r%}Yc">>,<<>>}]}}, {set,{var,53},{call,qc_leveldb,close,[{var,51}]}}, {set,{var,54},{call,qc_leveldb,reopen,[]}}, {set,{var,56},{call,qc_leveldb,put,[{var,54},{obj,<<>>,<<>>}]}}, {set,{var,60},{call,qc_leveldb,close,[{var,54}]}}, {set,{var,61},{call,qc_leveldb,reopen,[]}}, {set,{var,62},{call,qc_leveldb,delete,[{var,61},<<"l\r%}Yc">>]}},
{set,{var,64},
{call,qc_leveldb,delete,[{var,61},<<77,99,17,98,63,58,96,106,22,21>>]}},
{set,{var,65},{call,qc_leveldb,close,[{var,61}]}},
{set,{var,66},{call,qc_leveldb,reopen,[]}},
{set,{var,69},{call,qc_leveldb,delete,[{var,66},<<2,74,62,26>>]}},
{set,{var,72},{call,qc_leveldb,last,[{var,66}]}}]

COMMANDS:
"qc_statem-20111030-212350.erl"

HISTORY:
# 1:
Cmd: {set,{var,1},{call,qc_leveldb,open,[]}}
Reply: {ptr,{struct,leveldb_t},34376672}
State: {state,qc_statemc_lets,{state,false,false,undefined,[]}}

# 2:
Cmd: {set,{var,3},{call,qc_leveldb,close,[{var,1}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,{ptr,{struct,leveldb_t},34376672},[]}}

# 3:
Cmd: {set,{var,4},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34376784}
State: {state,qc_statemc_lets,{state,false,true,undefined,[]}}

# 4:
Cmd: {set,{var,5},{call,qc_leveldb,put,[{var,4},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,{ptr,{struct,leveldb_t},34376784},[]}}

# 5:
Cmd: {set,{var,7},{call,qc_leveldb,close,[{var,4}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34376784},
[{obj,<<>>,<<>>}]}}

# 6:
Cmd: {set,{var,11},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34374432}
State: {state,qc_statemc_lets,
{state,false,true,undefined,[{obj,<<>>,<<>>}]}}

# 7:
Cmd: {set,{var,16},{call,qc_leveldb,delete,[{var,11},<<"~88I.1">>]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374432},
[{obj,<<>>,<<>>}]}}

# 8:
Cmd: {set,{var,19},{call,qc_leveldb,put,[{var,11},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374432},
[{obj,<<>>,<<>>}]}}

# 9:
Cmd: {set,{var,25},{call,qc_leveldb,close,[{var,11}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374432},
[{obj,<<>>,<<>>}]}}

# 10:
Cmd: {set,{var,29},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34375728}
State: {state,qc_statemc_lets,
{state,false,true,undefined,[{obj,<<>>,<<>>}]}}

# 11:
Cmd: {set,{var,30},
{call,qc_leveldb,put,
[{var,29},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,127>>,
<<95,78,70,31,26>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34375728},
[{obj,<<>>,<<>>}]}}

# 12:
Cmd: {set,{var,33},{call,qc_leveldb,close,[{var,29}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34375728},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 13:
Cmd: {set,{var,34},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34413600}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 14:
Cmd: {set,{var,35},{call,qc_leveldb,put,[{var,34},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34413600},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 15:
Cmd: {set,{var,46},{call,qc_leveldb,close,[{var,34}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34413600},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 16:
Cmd: {set,{var,47},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34376640}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 17:
Cmd: {set,{var,49},{call,qc_leveldb,put,[{var,47},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34376640},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 18:
Cmd: {set,{var,50},{call,qc_leveldb,close,[{var,47}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34376640},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 19:
Cmd: {set,{var,51},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34370688}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 20:
Cmd: {set,{var,52},
{call,qc_leveldb,put,[{var,51},{obj,<<"l\r%`}Yc">>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34370688},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 21:
Cmd: {set,{var,53},{call,qc_leveldb,close,[{var,51}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34370688},
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 22:
Cmd: {set,{var,54},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34370656}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 23:
Cmd: {set,{var,56},{call,qc_leveldb,put,[{var,54},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34370656},
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 24:
Cmd: {set,{var,60},{call,qc_leveldb,close,[{var,54}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34370656},
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 25:
Cmd: {set,{var,61},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34415328}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 26:
Cmd: {set,{var,62},{call,qc_leveldb,delete,[{var,61},<<"l\r%}Yc">>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},34415328}, [{obj,<<"l\r%}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 27:
Cmd: {set,{var,64},
{call,qc_leveldb,delete,
[{var,61},<<77,99,17,98,63,58,96,106,22,21>>]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34415328},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 28:
Cmd: {set,{var,65},{call,qc_leveldb,close,[{var,61}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34415328},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 29:
Cmd: {set,{var,66},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34374880}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 30:
Cmd: {set,{var,69},{call,qc_leveldb,delete,[{var,66},<<2,74,62,26>>]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374880},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 31:
Cmd: {set,{var,72},{call,qc_leveldb,last,[{var,66}]}}
Reply: <<"l\r%`}Yc">>
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374880},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

RESULT:
{postcondition,false}

STATE:
{state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374880},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

STATE IS SANE:
true
false

Contributor

cmumford commented Sep 9, 2014

Comment #6 originally posted by josephwnorton on 2011-10-30T12:31:49.000Z:

Sanjay -

The previous patch did fix the previous issue. However, a new counterexample in 31 steps was found (and is repeatable). The failing post condition is same as previous issue - a reappearing ghost key.

[{init,{state,qc_statemc_lets,{state,false,false,undefined,[]}}},
{set,{var,1},{call,qc_leveldb,open,[]}},
{set,{var,3},{call,qc_leveldb,close,[{var,1}]}},
{set,{var,4},{call,qc_leveldb,reopen,[]}},
{set,{var,5},{call,qc_leveldb,put,[{var,4},{obj,<<>>,<<>>}]}},
{set,{var,7},{call,qc_leveldb,close,[{var,4}]}},
{set,{var,11},{call,qc_leveldb,reopen,[]}},
{set,{var,16},{call,qc_leveldb,delete,[{var,11},<<"~88I.1">>]}},
{set,{var,19},{call,qc_leveldb,put,[{var,11},{obj,<<>>,<<>>}]}},
{set,{var,25},{call,qc_leveldb,close,[{var,11}]}},
{set,{var,29},{call,qc_leveldb,reopen,[]}},
{set,{var,30},
{call,qc_leveldb,put,
[{var,29},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,127>>,
<<95,78,70,31,26>>}]}},
{set,{var,33},{call,qc_leveldb,close,[{var,29}]}},
{set,{var,34},{call,qc_leveldb,reopen,[]}},
{set,{var,35},{call,qc_leveldb,put,[{var,34},{obj,<<>>,<<>>}]}},
{set,{var,46},{call,qc_leveldb,close,[{var,34}]}},
{set,{var,47},{call,qc_leveldb,reopen,[]}},
{set,{var,49},{call,qc_leveldb,put,[{var,47},{obj,<<>>,<<>>}]}},
{set,{var,50},{call,qc_leveldb,close,[{var,47}]}},
{set,{var,51},{call,qc_leveldb,reopen,[]}},
{set,{var,52},{call,qc_leveldb,put,[{var,51},{obj,<<"l\r%}Yc">>,<<>>}]}}, {set,{var,53},{call,qc_leveldb,close,[{var,51}]}}, {set,{var,54},{call,qc_leveldb,reopen,[]}}, {set,{var,56},{call,qc_leveldb,put,[{var,54},{obj,<<>>,<<>>}]}}, {set,{var,60},{call,qc_leveldb,close,[{var,54}]}}, {set,{var,61},{call,qc_leveldb,reopen,[]}}, {set,{var,62},{call,qc_leveldb,delete,[{var,61},<<"l\r%}Yc">>]}},
{set,{var,64},
{call,qc_leveldb,delete,[{var,61},<<77,99,17,98,63,58,96,106,22,21>>]}},
{set,{var,65},{call,qc_leveldb,close,[{var,61}]}},
{set,{var,66},{call,qc_leveldb,reopen,[]}},
{set,{var,69},{call,qc_leveldb,delete,[{var,66},<<2,74,62,26>>]}},
{set,{var,72},{call,qc_leveldb,last,[{var,66}]}}]

COMMANDS:
"qc_statem-20111030-212350.erl"

HISTORY:
# 1:
Cmd: {set,{var,1},{call,qc_leveldb,open,[]}}
Reply: {ptr,{struct,leveldb_t},34376672}
State: {state,qc_statemc_lets,{state,false,false,undefined,[]}}

# 2:
Cmd: {set,{var,3},{call,qc_leveldb,close,[{var,1}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,{ptr,{struct,leveldb_t},34376672},[]}}

# 3:
Cmd: {set,{var,4},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34376784}
State: {state,qc_statemc_lets,{state,false,true,undefined,[]}}

# 4:
Cmd: {set,{var,5},{call,qc_leveldb,put,[{var,4},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,{ptr,{struct,leveldb_t},34376784},[]}}

# 5:
Cmd: {set,{var,7},{call,qc_leveldb,close,[{var,4}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34376784},
[{obj,<<>>,<<>>}]}}

# 6:
Cmd: {set,{var,11},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34374432}
State: {state,qc_statemc_lets,
{state,false,true,undefined,[{obj,<<>>,<<>>}]}}

# 7:
Cmd: {set,{var,16},{call,qc_leveldb,delete,[{var,11},<<"~88I.1">>]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374432},
[{obj,<<>>,<<>>}]}}

# 8:
Cmd: {set,{var,19},{call,qc_leveldb,put,[{var,11},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374432},
[{obj,<<>>,<<>>}]}}

# 9:
Cmd: {set,{var,25},{call,qc_leveldb,close,[{var,11}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374432},
[{obj,<<>>,<<>>}]}}

# 10:
Cmd: {set,{var,29},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34375728}
State: {state,qc_statemc_lets,
{state,false,true,undefined,[{obj,<<>>,<<>>}]}}

# 11:
Cmd: {set,{var,30},
{call,qc_leveldb,put,
[{var,29},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,127>>,
<<95,78,70,31,26>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34375728},
[{obj,<<>>,<<>>}]}}

# 12:
Cmd: {set,{var,33},{call,qc_leveldb,close,[{var,29}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34375728},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 13:
Cmd: {set,{var,34},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34413600}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 14:
Cmd: {set,{var,35},{call,qc_leveldb,put,[{var,34},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34413600},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 15:
Cmd: {set,{var,46},{call,qc_leveldb,close,[{var,34}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34413600},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 16:
Cmd: {set,{var,47},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34376640}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 17:
Cmd: {set,{var,49},{call,qc_leveldb,put,[{var,47},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34376640},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 18:
Cmd: {set,{var,50},{call,qc_leveldb,close,[{var,47}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34376640},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 19:
Cmd: {set,{var,51},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34370688}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 20:
Cmd: {set,{var,52},
{call,qc_leveldb,put,[{var,51},{obj,<<"l\r%`}Yc">>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34370688},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 21:
Cmd: {set,{var,53},{call,qc_leveldb,close,[{var,51}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34370688},
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 22:
Cmd: {set,{var,54},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34370656}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 23:
Cmd: {set,{var,56},{call,qc_leveldb,put,[{var,54},{obj,<<>>,<<>>}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34370656},
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 24:
Cmd: {set,{var,60},{call,qc_leveldb,close,[{var,54}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34370656},
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 25:
Cmd: {set,{var,61},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34415328}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<"l\r%`}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 26:
Cmd: {set,{var,62},{call,qc_leveldb,delete,[{var,61},<<"l\r%}Yc">>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},34415328}, [{obj,<<"l\r%}Yc">>,<<>>},
{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 27:
Cmd: {set,{var,64},
{call,qc_leveldb,delete,
[{var,61},<<77,99,17,98,63,58,96,106,22,21>>]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34415328},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 28:
Cmd: {set,{var,65},{call,qc_leveldb,close,[{var,61}]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34415328},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 29:
Cmd: {set,{var,66},{call,qc_leveldb,reopen,[]}}
Reply: {ptr,{struct,leveldb_t},34374880}
State: {state,qc_statemc_lets,
{state,false,true,undefined,
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 30:
Cmd: {set,{var,69},{call,qc_leveldb,delete,[{var,66},<<2,74,62,26>>]}}
Reply: true
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374880},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

# 31:
Cmd: {set,{var,72},{call,qc_leveldb,last,[{var,66}]}}
Reply: <<"l\r%`}Yc">>
State: {state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374880},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,
127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

RESULT:
{postcondition,false}

STATE:
{state,qc_statemc_lets,
{state,false,true,
{ptr,{struct,leveldb_t},34374880},
[{obj,<<98,66,22,50,78,96,90,21,61,48,126,34,1,65,127>>,
<<95,78,70,31,26>>},
{obj,<<>>,<<>>}]}}

STATE IS SANE:
true
false

@cmumford

This comment has been minimized.

Show comment
Hide comment
@cmumford

cmumford Sep 9, 2014

Contributor

Comment #7 originally posted by josephwnorton on 2011-11-01T17:31:20.000Z:

Please close this issue - thanks!

Contributor

cmumford commented Sep 9, 2014

Comment #7 originally posted by josephwnorton on 2011-11-01T17:31:20.000Z:

Please close this issue - thanks!

@cmumford

This comment has been minimized.

Show comment
Hide comment
@cmumford

cmumford Sep 9, 2014

Contributor

Comment #8 originally posted by dgrogan@chromium.org on 2011-11-07T21:24:38.000Z:

<empty>

Contributor

cmumford commented Sep 9, 2014

Comment #8 originally posted by dgrogan@chromium.org on 2011-11-07T21:24:38.000Z:

<empty>

@cmumford cmumford closed this Sep 9, 2014

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment