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()) ?