| Patch | Description | Author | Forwarded | Bugs | Origin | Last update |
|---|---|---|---|---|---|---|
| 0001-Do-not-install-redundant-files.patch | Do not install redundant files | Stephane Glondu <steph@glondu.net> | no | 2015-02-12 | ||
| 0002-Retry-waitpid-if-it-fails-with-EINTR.patch | Retry waitpid if it fails with EINTR | Martin Jambon <martin@mjambon.com> | no | 2011-12-30 | ||
| 0003-possible-fix-for-concurrent-access-to-the-input-stre.patch | possible fix for concurrent access to the input stream in the master process, there are threads 1-to-1 associated with workers. They concurrently try to pull a task from a stream [in_stream] and send it to a worker, providing a waiter thread for delivering the output. However it seems that several worker-associated threads can read the same incoming value in the stream, perform the computation concurrently and try to send it back to the waiter. Since the waiter is woken up several times, this generates the exceptions [Invalid_argument("Lwt.wakeup_result")]. The final result is correct, but ressources are wasted, since some computation may be several times by several workers (and that really happens, since the exceptions are raised quite a few times). The proposed fix is to add a mutex for the access to [in_stream]. |
pveber <philippe.veber@gmail.com> | no | 2013-04-01 | ||
| 0004-slightly-more-efficient-fix-for-concurrent-access-to.patch | slightly more efficient fix for concurrent access to [in_stream] now each pool has its own mutex. |
pveber <philippe.veber@gmail.com> | no | 2013-04-01 |