RTX timer tick rate

Hello,

I was wondering if any of you uses RTX with a tick rate faster than 10 milliseconds. Franc Urbanc, RTX's author, recommends this setting but I am not sure why - a context switch overhead of a LPC2478 running at 72[MHz] will be about 6 microseconds. However, when we try to set the tick rate to 1 millisecond or 100 microsecond, RTX seems to hang after about 10 minutes (when at 100 microseconds) in this code:

void os_put_prio (P_XCB p_CB, P_TCB p_task) {
   /* Put task identified with "p_task" into list ordered by priority.       */
   /* "p_CB" points to head of list; list has always an element at end with  */
   /* a priority less than "p_task->prio".                                   */
.
.
.
  /* Search for an entry in the list */
   while (p_CB2 != NULL && prio <= p_CB2->prio) {
      p_CB = (P_XCB)p_CB2;
      p_CB2 = p_CB2->p_lnk;
   }

sometimes, we see only one entry in the linked list whose left and right pointer point to the entry itself, resulting in a system deadlock. Yes, we probably can get away with a tick rate of 10 milliseconds, but I would appreciate your insight anyway.