A question regarding thread creation in L4Linux.

[Сергей Грехов]

Hello to everyone!
The question is about method l4lx_thread_create() from ports-foc/src/lib/l4lx/l4lx_thread.cc.
According to the thread creation procedure in L4lx library, the pointer to VCPU instances are saved in a static array
                   static L4lx::Vcpu* vcpus[L4LX_THREAD_NO_THREADS];
The index within this array is defined by passing UTCB address to function thread_id(). Now, if enable SMP and set two VCPUs, one can see the following strange thing:

//creating cpu0
l4lx_thread_create: (vc->utcb() = 44000400) thread_id() = 00000002 TID = 00011000
//everything is fine: pointer to Vcpu instance is saved under id=2

//creating timer
l4lx_thread_create: (vc->utcb() = 44000600) thread_id() = 00000001 TID = 00015000
//everything is fine here too: pointer to Vcpu instance is saved under id=1

//creating cpu1
l4lx_thread_create: (vc->utcb() = 44000800) thread_id() = 00000002 TID = 00019000
//something weird is happening here: pointer to Vcpu instance is saved under id=2, previous pointer is lost.

Looking inside thread_id() one can find that it uses utcb_base_addr() [which is equal to l4_utcb()] to calculate required index in array. Is it a bug? Should not the utcb_base_addr() be something similar to following expression:
                (Genode::Native_config::context_area_virtual_base() + THREAD_MAX * Genode::Native_config::context_virtual_size()) ?

-- 
Best regards,
Sergey S. Grekhov