+ /*
+ * The kernel file `include/linux/mmu_notifier.h` states the following
+ * regarding the invalidate_range_start() callback:
+ *
+ * If blockable argument is set to false then the callback cannot
+ * sleep and has to return with -EAGAIN. 0 should be returned
+ * otherwise.
+ *
+ * The following function executes spin_lock_irqsave(), which feels like it
+ * qualifies as 'sleep'. However, returning -EAGAIN would require me to
+ * understand the location and function of all code that calls this
+ * callback. I do not yet have that understanding.
+ *
+ * For now, maintain the original behavior of calling
+ * micscif_rma_destroy_tcw() every time, accepting the spinlock. If this
+ * becomes problematic, either figure out all the code that can call this
+ * function and teach it to understand -EAGAIN, or investigate the `#ifdef
+ * CONFIG_MMU_NOTIFIER`.
+ *
+ * If you ended up here while tracking down a bug and pulling your hair
+ * out, sorry. :-(
+ */