[klee-dev] Dummy pthread library?

[Alastair Reid]

Hi Cristian,

I have implemented the pthread subset needed by Rust - supporting only one
thread and query functions return 0/NULL.
https://github.com/klee/klee/compare/master...alastairreid:pthread_stub?expand=1
However, it turns out that this was not the cause of any problems (apart
from some warning messages) so I am not sure that it is worth having this
change.
I'm happy to submit a pull request (eg by clicking the button in the above
link) if you think it useful - but I suspect that it is not useful.

But, I have submitted a PR for the issue that was causing me problems: Rust
invokes a weak function pointer __cxa_thread_atexit_impl

--
Alastair


On Thu, Jul 30, 2020 at 8:03 PM Cristian Cadar <c.cadar at imperial.ac.uk>
wrote:

> Hi again Alastair,
>
> I'm not aware of anything like this, but it would be a nice extension of
> KLEE's POSIX environment.
>
> Best,
> Cristian
>
> On 30/07/2020 17:37, Alastair Reid wrote:
> > Is there a dummy pthread library that I can use with single-threaded
> > programs that only use a single thread but are linked against
> > thread-safe libraries (i.e., threads that call pthread_* functions).
> >
> > I am 99.9% sure that I don't need any actual thread support - just an
> > implementation that pretends to support a single thread.
> > I'm guessing that a dummy library would mostly consist of a bunch of
> > functions that return constant values because there is only one thread,
> > no lock contention, etc.
> > And I'm also guessing that somebody has already implemented such a
> library.
> >
> > --
> > Alastair Reid
> >
> > ps The functions that I need (as reported when I run KLEE) are:
> >
> >    pthread_attr_destroy
> >    pthread_attr_getstack
> >    pthread_attr_init
> >    pthread_cond_destroy
> >    pthread_cond_init
> >    pthread_cond_signal
> >    pthread_cond_wait
> >    pthread_condattr_destroy
> >    pthread_condattr_init
> >    pthread_condattr_setclock
> >    pthread_getattr_np
> >    pthread_getspecific
> >    pthread_key_create
> >    pthread_key_delete
> >    pthread_mutex_destroy
> >    pthread_mutex_init
> >    pthread_mutex_lock
> >    pthread_mutex_unlock
> >    pthread_mutexattr_destroy
> >    pthread_mutexattr_init
> >    pthread_mutexattr_settype
> >    pthread_rwlock_rdlock
> >    pthread_rwlock_unlock
> >    pthread_rwlock_wrlock
> >    pthread_self
> >    pthread_setspecific
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at imperial.ac.uk
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> >
>
-------------- next part --------------
HTML attachment scrubbed and removed