[seL4] Strange behavior when writing to memory mapped to a custom device in the VMM.

8 Sep 2018

      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