Deferred Interrupt Processing and posting a Binary Semaphore more than once

Hmmm. That makes me think that a Method 3 could really be helpful. I see that there’s already a pxTopOfStack and (potentially) a pxEndOfStack:

typedef struct tskTaskControlBlock       /* The old naming convention is used to prevent breaking kernel aware debuggers. */
{
volatile StackType_t * pxTopOfStack; /*< Points to the location of the last item placed on the tasks stack.  THIS MUST BE THE FIRST MEMBER OF THE TCB STRUCT. */

//...
    #if ( ( portSTACK_GROWTH > 0 ) || ( configRECORD_STACK_HIGH_ADDRESS == 1 ) )
        StackType_t * pxEndOfStack; /*< Points to the highest valid address for the stack. */
    #endif

Seems to me that comparing pxTopOfStack to pxEndOfStack would be quite efficient (a couple of machine instructions). Maybe efficient enough that it could be done every time something is placed on the stack? If not maybe something like another pointer in the tskTaskControlBlock (e.g., pxStackHighWaterMark) could record the highest (or lowest, depending on portSTACK_GROWTH) pxTopOfStack for later comparison?