/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    SpinLockRelease

Domain:

    storport

Rule ID:

    Not Applicable

Description:

    This rule verifies that the driver does not attempt to release a lock via 
    KeReleaseSpinLock without first acquiring it via KeAquireSpinlock 
    or KeAcquireSpinLockRaiseToDpc. The rule passes when the acquired spin lock
    is released.

Help Link:

    https://go.microsoft.com/fwlink/?LinkId=507369

--*/



#include "ntddk_slic.h"

state {
	enum {unlocked,locked} s = unlocked;
	int *pointer = 0;
}


KeReleaseSpinLock.entry
{
	if (s == unlocked && pointer != $1) {
		abort "The driver is calling $fname without first acquiring the spin lock.";
	} else {
		halt;
	}
}

[
KeAcquireSpinLock,
KeAcquireSpinLockRaiseToDpc
].exit
{
	s = locked;
	pointer = $1;
}
