Re: [PATCH v2 1/2] mm: improve readability of transparent_hugepage_enabled()

[Vlastimil Babka <vbabka@xxxxxxx>]

On 06/14/2017 07:02 PM, Dan Williams wrote:
> On Wed, Jun 14, 2017 at 9:53 AM, Vlastimil Babka <vbabka@xxxxxxx> wrote:
> 
> Can you share the test-thp.c so I can add this to my test collection?

Attached.

> I'm assuming cbmc is "Bounded Model Checker for C/C++"?

Yes. This blog from Paul inspired me:
http://paulmck.livejournal.com/38997.html

Works nicely, just if it finds a bug, the counterexamples are a bit of
PITA to decipher :)

Vlastimil

#include <stdbool.h>
#include <stdio.h>

#define VM_GROWSDOWN    0x00000100      /* general info on the segment */
#define VM_HUGEPAGE     0x20000000      /* MADV_HUGEPAGE marked this vma */
#define VM_NOHUGEPAGE   0x40000000      /* MADV_NOHUGEPAGE marked this vma */
#define VM_ARCH_1       0x01000000      /* Architecture-specific flag */
#define VM_GROWSUP VM_ARCH_1
#define VM_SEQ_READ     0x00008000      /* App will access data sequentially */
#define VM_RAND_READ    0x00010000      /* App will not benefit from clustered reads */
#define VM_STACK_INCOMPLETE_SETUP       (VM_RAND_READ | VM_SEQ_READ)

enum transparent_hugepage_flag {
        TRANSPARENT_HUGEPAGE_FLAG,
        TRANSPARENT_HUGEPAGE_REQ_MADV_FLAG,
        TRANSPARENT_HUGEPAGE_DEFRAG_DIRECT_FLAG,
        TRANSPARENT_HUGEPAGE_DEFRAG_KSWAPD_FLAG,
        TRANSPARENT_HUGEPAGE_DEFRAG_KSWAPD_OR_MADV_FLAG,
        TRANSPARENT_HUGEPAGE_DEFRAG_REQ_MADV_FLAG,
        TRANSPARENT_HUGEPAGE_DEFRAG_KHUGEPAGED_FLAG,
        TRANSPARENT_HUGEPAGE_USE_ZERO_PAGE_FLAG,
        TRANSPARENT_HUGEPAGE_DEBUG_COW_FLAG,
};

unsigned long transparent_hugepage_flags;
struct vm_area_struct {
	unsigned long vm_flags;
};

bool is_vma_temporary_stack(struct vm_area_struct *vma)
{
        int maybe_stack = vma->vm_flags & (VM_GROWSDOWN | VM_GROWSUP);

        if (!maybe_stack)
                return false;

        if ((vma->vm_flags & VM_STACK_INCOMPLETE_SETUP) ==
                                                VM_STACK_INCOMPLETE_SETUP)
                return true;

        return false;
}

#define transparent_hugepage_enabled1(__vma)				\
	((transparent_hugepage_flags &					\
	  (1<<TRANSPARENT_HUGEPAGE_FLAG) ||				\
	  (transparent_hugepage_flags &					\
	   (1<<TRANSPARENT_HUGEPAGE_REQ_MADV_FLAG) &&			\
	   ((__vma)->vm_flags & VM_HUGEPAGE))) &&			\
	 !((__vma)->vm_flags & VM_NOHUGEPAGE) &&			\
	 !is_vma_temporary_stack(__vma))

// v2
static inline bool transparent_hugepage_enabled2(struct vm_area_struct *vma)
{
	if ((vma->vm_flags & VM_NOHUGEPAGE) || is_vma_temporary_stack(vma))
		return false;

	if (transparent_hugepage_flags & (1 << TRANSPARENT_HUGEPAGE_FLAG))
		return true;

	if (transparent_hugepage_flags &
				(1 << TRANSPARENT_HUGEPAGE_REQ_MADV_FLAG))
		return !!(vma->vm_flags & VM_HUGEPAGE);

	return false;
}

// v1
static inline bool transparent_hugepage_enabled3(struct vm_area_struct *vma)
{
	if (transparent_hugepage_flags & (1 << TRANSPARENT_HUGEPAGE_FLAG))
		return true;

	if (transparent_hugepage_flags
			& (1 << TRANSPARENT_HUGEPAGE_REQ_MADV_FLAG))
		/* check vma flags */;
	else
		return false;

	if ((vma->vm_flags & (VM_HUGEPAGE | VM_NOHUGEPAGE)) == VM_HUGEPAGE
			&& !is_vma_temporary_stack(vma))
		return true;

	return false;
}

int main(int argc, char *argv[])
{
	struct vm_area_struct vma;

	vma.vm_flags = (unsigned long) argv[1];
	transparent_hugepage_flags = (unsigned long) argv[2];

//	assert(transparent_hugepage_enabled1(&vma)
//			== transparent_hugepage_enabled2(&vma));
	assert(transparent_hugepage_enabled1(&vma)
			== transparent_hugepage_enabled3(&vma));
}