ticktac-project/tchecker

Problem arising when pool_t::destruct_all() is not called

fredher opened this issue · 3 comments

It looks like the destructor of the zg pool destroys _zone_pool before the ta allocator is destroyed

From Alexandre Duret-Lutz:

J'ai des problèmes lorsque je n'appelle pas ~destruct_all(), typiquement :

==13412== Invalid read of size 4
==13412==    at 0x121366: release_reference
(tchecker/include/tchecker/utils/shared_objects.hh:182)
==13412==    by 0x121366: reset
(tchecker/include/tchecker/utils/shared_objects.hh:473)
==13412==    by 0x121366: ~intrusive_shared_ptr_t
(tchecker/include/tchecker/utils/shared_objects.hh:399)
==13412==    by 0x121366: ~state_t
(tchecker/include/tchecker/zg/details/state.hh:74)
==13412==    by 0x121366: ~make_shared_t
(tchecker/include/tchecker/utils/shared_objects.hh:226)
==13412==    by 0x121366: destruct
(tchecker/include/tchecker/utils/shared_objects.hh:114)
==13412==    by 0x121366: destruct_all
(tchecker/include/tchecker/utils/pool.hh:240)
==13412==    by 0x121366: ~pool_t (tchecker/include/tchecker/utils/pool.hh:126)
==13412==    by 0x121366: ~state_pool_allocator_t
(tchecker/include/tchecker/ts/allocators.hh:80)
==13412==    by 0x121366: ~state_pool_allocator_t
(tchecker/include/tchecker/fsm/details/allocators.hh:93)
==13412==    by 0x121366: ~state_pool_allocator_t
(tchecker/include/tchecker/ta/details/allocators.hh:33)
==13412==    by 0x121366: ~state_pool_allocator_t
(tchecker/include/tchecker/zg/details/allocators.hh:113)
==13412==    by 0x121366: ~state_pool_allocator_t
(tchecker/include/tchecker/zg/zg_ta.hh:143)
==13412==    by 0x121366: ~allocator_t
(tchecker/include/tchecker/ts/allocators.hh:255)
==13412==    by 0x121366: tcltl_kripke::~tcltl_kripke() (tcltl/tcltl.cc:216)
==13412==    by 0x1234F7: _M_release
(/usr/include/c++/9/bits/shared_ptr_base.h:155)
==13412==    by 0x1234F7:
std::_Sp_counted_base<(__gnu_cxx::_Lock_policy)2>::_M_release()
(/usr/include/c++/9/bits/shared_ptr_base.h:148
)
==13412==    by 0x11EA39: ~__shared_count
(/usr/include/c++/9/bits/shared_ptr_base.h:730)
==13412==    by 0x11EA39: ~__shared_ptr
(/usr/include/c++/9/bits/shared_ptr_base.h:1169)
==13412==    by 0x11EA39: ~shared_ptr (/usr/include/c++/9/bits/shared_ptr.h:103)
==13412==    by 0x11EA39: main (tcltl/tcltl.cc:718)
==13412==  Address 0x698f048 is 8 bytes inside a block of size 7,200,008 free'd
==13412==    at 0x483758B: operator delete[](void*)
(coregrind/m_replacemalloc/vg_replace_malloc.c:651)
==13412==    by 0x121212: free_all (tchecker/include/tchecker/utils/pool.hh:264)
==13412==    by 0x121212: destruct_all
(tchecker/include/tchecker/utils/pool.hh:246)
==13412==    by 0x121212: ~pool_t (tchecker/include/tchecker/utils/pool.hh:126)
==13412==    by 0x121212: ~state_pool_allocator_t
(tchecker/include/tchecker/zg/details/allocators.hh:113)
==13412==    by 0x121212: ~state_pool_allocator_t
(tchecker/include/tchecker/zg/zg_ta.hh:143)
==13412==    by 0x121212: ~allocator_t
(tchecker/include/tchecker/ts/allocators.hh:255)
==13412==    by 0x121212: tcltl_kripke::~tcltl_kripke() (tcltl/tcltl.cc:216)
==13412==    by 0x1234F7: _M_release
(/usr/include/c++/9/bits/shared_ptr_base.h:155)
==13412==    by 0x1234F7:
std::_Sp_counted_base<(__gnu_cxx::_Lock_policy)2>::_M_release()
(/usr/include/c++/9/bits/shared_ptr_base.h:148
)
==13412==    by 0x11EA39: ~__shared_count
(/usr/include/c++/9/bits/shared_ptr_base.h:730)
==13412==    by 0x11EA39: ~__shared_ptr
(/usr/include/c++/9/bits/shared_ptr_base.h:1169)
==13412==    by 0x11EA39: ~shared_ptr (/usr/include/c++/9/bits/shared_ptr.h:103)
==13412==    by 0x11EA39: main (tcltl/tcltl.cc:718)

Ce que je comprends c'est que le destructeur de l'allocateur de zg
détruit d'abord _zone_pool avant de détruire l'allocateur de ta,
alors que destruct_all() fait ça dans l'autre sens et que ça semble se
passer mieux.

Could you please check if commit 3231a1a fixes the error?

adl commented

It does, thank you.