Hi Dan, It is likely that the instruction that is causing the fault is not being decoded by hardware or software.  ARM has done a reasonable job in providing hardware support for decoding faulting instructions, but only a subset of the ISA is supported. The instruction causing the fault might be a load with increment (*pArray++). A trivial fix might be to rewrite your code as:  #define idx(i) (i%16)   for(i = 0; i < buf->capacity() && buf->capacity() > 16; i++){     mem[idx(i)] = *pArray[i];   } Failing that, I recommend using objdump to identify the faulting instruction and follow the code path in ../projects/seL4_projects_libs/libsel4arm-vmm/src/fault.c: get_rt: 357 to see how that particular instruction is being decoded and handled. - Alex Kroh From: Devel on behalf of Dan DaCosta Sent: Saturday, September 8, 2018 4:19 AM To: devel@sel4.systems Cc: Darren Cofer Subject: [seL4] Strange behavior when writing to memory mapped to a custom device in the VMM.   To Whom It May Concern: I am observing seL4+VM+ARM behavior on the TK1-SOM that I find very puzzling. Consider the following code:   #define idx(i) (i%16)   for(i = 0; i < buf->capacity() && buf->capacity() > 16; i++, pArray++){     mem[idx(i)] = *pArray;   } where 'pArray' is the array representation of 'buf' and 'mem' is a memory mapped page set that corresponds to a page set of memory that is managed by a fault handler in the VMM (something I have installed myself using a 'DEV_CUSTOM' device). This code runs as I would expect. However, the follow code results in an assertion failure in the VMM:   #define idx(i) (i%16)   for(i = 0; i < 16; i++, pArray++){     mem[idx(i)] = *pArray;   } The error report follows:   32 bit ARM insts not decoded   --------   Pagefault from [Linux]: write fault @ PC: 0xbd7499a8 IPA: 0xe0001000, FSR: 0x2000046   Context:   r0: 0xb6d2a050   r1: 0x0   r2: 0xb6ac76b8   r3: 0x4c   r4: 0xb6d2a050   r5: 0xb6d2a8ec   r6: 0x1   r7: 0xb6d2a050   r8: 0x7fb73000   r9: 0xad13cfff   r10: 0xabe31310   r11: 0x19   r12: 0xb6d285d8   pc: 0x7f68f9a8   r14: 0x7f68f99c   sp: 0xaf1c3c20   cpsr: 0x80000010   --------   Assertion failed: rt >= 0 (../projects/seL4_projects_libs/libsel4arm-vmm/src/fault.c: get_rt: 357)   Some added information that may be helpful; if the strange modulo operation I am performing on the index is removed I receive a similar crash for both code snippets. Any thoughts on where I might look to get to the bottom of this problem would be helpful. Thanks! Dan DaCosta