Page table corruption after requesting non-conventional memory from sigma0 on x86-64 SMP

Hi,

It seems that the page table is corrupted after a program requesting 
some non-conventional memory under x86-64 SMP.

Here is a test case to reproduce the problem. The program would execute 
successfully. However, when I try to dump the page table in KDB, the 
output goes as follows:


 > ptab
Space [current]: 0000003a00000001
CPU id [0]: 0
Memory area (Complete/User/Kernel(w/o tcb&remap)/Tcb/Remap/Manual) 
[complete]: complete
0000000000000000 [0000000000c3e027]: tree=ffffffffc0c3e000
0000000000000000 [0000000000c46027]:   tree=ffffffffc0c46000
0000000002000000 [0000000000c48027]:     tree=ffffffffc0c48000
0000000002000000 [0000000002000027]:       phys=0000000002000000  
map=ffffffffc0c47028   4KB rw~ (R~X) user WB
0000000002001000 [0000000002001027]:       phys=0000000002001000  
map=ffffffffc0c47088   4KB rw~ (R~X) user WB
0000000002011000 [0000000002011067]:       phys=0000000002011000  
map=ffffffffc0c47040   4KB rw~ (RWX) user WB
0000000080000000 [0000000000c3f027]:   tree=ffffffffc0c3f000
00000000bf000000 [0000000000c44027]:     tree=ffffffffc0c44000
00000000bf000000 [0000000000c42067]:       phys=0000000000c42000  
map=00000000bf000000   4KB rw~ (RWX) user WB
00000000bfe00000 [0000000000c40027]:     tree=ffffffffc0c40000
00000000bff00000 [000000000062e025]:       phys=000000000062e000  
map=00000000bff00000   4KB r~~ (R~X) user WB
00000000c0000000 [0000000000c4d007]:   tree=ffffffffc0c4d000
L4 Kernel BUG: X64 shouldn't have non-global superpages
Not implemented: word_t pgent_t::smp_reference_bits(space_t*, 
pgent_t::pgsize_e, void*)
/home/mai4/work/dOS/src/dOS/l4ka/kernel/src/glue/v4-x86/x64/space.cc, 
line 110

I've no idea where to look at. Any suggestions are highly appreciated.

Haohui

#include <l4io.h>
#include <l4/ipc.h>
#include <l4/sigma0.h>

int main(int argc, char * argv[]) {
  L4_Word_t phy_addr_base = 0xf0000000;
  L4_Word_t size = 1 << 22; // 4M
  L4_Fpage_t rfpage = L4_Fpage( (L4_Word_t) phy_addr_base, size);
  L4_Set_Rights( &rfpage, L4_FullyAccessible);
  L4_Fpage_t res = L4_Sigma0_GetPage(L4_nilthread, rfpage);
  printf("Done mapping\n");
  L4_Sleep(L4_Never);
  return 0;
}