[klee-dev] Cloud9 and KLEE - POSIX features

[Carril Rodríguez, Luis Manuel (IPD)]

Hi,
    I made a port one year ago of the multithread POSIX model of Cloud9 to KLEE v1.0: https://github.com/lmcarril/klee
    I sent at the moment a pull request, but did not go forward.
    I used the multithreaded version myself as a base to build a KLEE based race detector.
    As far as I know, no other POSIX capabilities of Cloud9 have been ported to the new version.

Cheers
Luis M

-----Ursprüngliche Nachricht-----
Von: klee-dev-bounces at imperial.ac.uk [mailto:klee-dev-bounces at imperial.ac.uk] Im Auftrag von Marko Dimjaševic
Gesendet: Freitag, 24. Juni 2016 04:11
An: KLEE dev mailing list <klee-dev at imperial.ac.uk>
Betreff: [klee-dev] Cloud9 and KLEE - POSIX features

Dear KLEE developers,

Can anyone comment on what's the connection between the POSIX runtime in KLEE and in Cloud9?

As mentioned in a paper on Cloud9:

http://doi.acm.org/10.1145/1966445.1966463

Cloud9 builds on KLEE. Have some or all POSIX features from Cloud9 been back-ported to KLEE?

The paper was published in 2011 so I'm trying to understand the timeline of how KLEE and Cloud9 developed.

For example, the paper mentions that unlike KLEE, Cloud9 supports network and pipe parts of POSIX.

My hunch is those features haven't been ported back to KLEE, yet Cloud9 seems to be an outdated project, at least according to a commit history of its Git repository:

https://github.com/dslab-epfl/cloud9


It would be nice to have these features in KLEE, but probably no one found time, energy, motivation, or all of it to make it happen.


--
Regards,
Marko Dimjašević <marko at cs.utah.edu> .   University of Utah
https://dimjasevic.net/marko         . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org