Trouble with semaphore library

[Marc CHALAND]

Hello,

I encounter strange problems with semaphore library from l4env. I use
a vanillia revision 230 on an intel PIII architecture. After some
debugging and tracing, I get the following scenarion :

1. thread 03 of my process calls a semaphore down timed which then
calls BLOCKTIMED IPC to semaphore thread 02. So semaphore structure is:
 counter = -1
 pending = 0
 queue = 03

2. thread 08 calls semaphore_up inline assembler code. Before IPC
call, the semaphore structure is as follow :
 counter = 0
 pending = 0
 queue = 03

3. Thread 03 gains the CPU after timeout and calls IPC RELEASETIMED :
 counter = 1
 pending = 0
 queue = empty

4. Thread 02 doesn't find thread into queue, so that pending is set to 1.
 counter = 1
 pending = 1
 queue = empty

5. Thread 03 calls semaphore_down. No IPC is called.
 counter = 0
 pending = 1
 queue = empty

6. Thread 03 calls semaphore_down again and IPC BLOCK is called. IPC
awakes imediately 03 with a counter value of -1 and nobody into queue.
 counter = -1
 pending = 0
 queue = empty

It seems to me that this state is not normal. Do you agree ? Is this
scenario possible as I observe clearly state 4 5 and 6 ? What pending
is for ?

Thanks in advance for your answers.
Marc