diff --git a/Kernel/MemoryManager.cpp b/Kernel/MemoryManager.cpp
index beca4e6ca7..bdea62f373 100644
--- a/Kernel/MemoryManager.cpp
+++ b/Kernel/MemoryManager.cpp
@@ -241,7 +241,7 @@ void MemoryManager::flushEntireTLB()
 
 void MemoryManager::flushTLB(LinearAddress laddr)
 {
-    asm volatile("invlpg %0": :"m" (*(char*)laddr.get()));
+    asm volatile("invlpg %0": :"m" (*(char*)laddr.get()) : "memory");
 }
 
 void MemoryManager::map_region_at_address(PageDirectory* page_directory, Region& region, LinearAddress laddr, bool user_allowed)
diff --git a/Kernel/ProcFileSystem.cpp b/Kernel/ProcFileSystem.cpp
index e85cc87a9a..45cb6da3d2 100644
--- a/Kernel/ProcFileSystem.cpp
+++ b/Kernel/ProcFileSystem.cpp
@@ -4,6 +4,7 @@
 #include "system.h"
 #include "MemoryManager.h"
 #include "StdLib.h"
+#include "i386.h"
 
 static ProcFileSystem* s_the;
 
@@ -177,6 +178,71 @@ ByteBuffer procfs$mounts()
     return buffer;
 }
 
+ByteBuffer procfs$cpuinfo()
+{
+    auto buffer = ByteBuffer::createUninitialized(256);
+    char* ptr = (char*)buffer.pointer();
+    {
+        CPUID cpuid(0);
+        ptr += ksprintf(ptr, "cpuid:     ");
+        auto emit_dword = [&] (dword value) {
+            ptr += ksprintf(ptr, "%c%c%c%c",
+                value & 0xff,
+                (value >> 8) & 0xff,
+                (value >> 16) & 0xff,
+                (value >> 24) & 0xff);
+        };
+        emit_dword(cpuid.ebx());
+        emit_dword(cpuid.edx());
+        emit_dword(cpuid.ecx());
+        ptr += ksprintf(ptr, "\n");
+    }
+    {
+        CPUID cpuid(1);
+        dword stepping = cpuid.eax() & 0xf;
+        dword model = (cpuid.eax() >> 4) & 0xf;
+        dword family = (cpuid.eax() >> 8) & 0xf;
+        dword type = (cpuid.eax() >> 12) & 0x3;
+        dword extended_model = (cpuid.eax() >> 16) & 0xf;
+        dword extended_family = (cpuid.eax() >> 20) & 0xff;
+        dword display_model;
+        dword display_family;
+        if (family == 15) {
+            display_family = family + extended_family;
+            display_model = model + (extended_model << 4);
+        } else if (family == 6) {
+            display_family = family;
+            display_model = model + (extended_model << 4);
+        } else {
+            display_family = family;
+            display_model = model;
+        }
+        ptr += ksprintf(ptr, "family:    %u\n", display_family);
+        ptr += ksprintf(ptr, "model:     %u\n", display_model);
+        ptr += ksprintf(ptr, "stepping:  %u\n", stepping);
+        ptr += ksprintf(ptr, "type:      %u\n", type);
+    }
+    {
+        // FIXME: Check first that this is supported by calling CPUID with eax=0x80000000
+        //        and verifying that the returned eax>=0x80000004.
+        char buffer[48];
+        dword* bufptr = reinterpret_cast<dword*>(buffer);
+        auto copy_brand_string_part_to_buffer = [&] (dword i) {
+            CPUID cpuid(0x80000002 + i);
+            *bufptr++ = cpuid.eax();
+            *bufptr++ = cpuid.ebx();
+            *bufptr++ = cpuid.ecx();
+            *bufptr++ = cpuid.edx();
+        };
+        copy_brand_string_part_to_buffer(0);
+        copy_brand_string_part_to_buffer(1);
+        copy_brand_string_part_to_buffer(2);
+        ptr += ksprintf(ptr, "brandstr:  \"%s\"\n", buffer);
+    }
+    buffer.trim(ptr - (char*)buffer.pointer());
+    return buffer;
+}
+
 ByteBuffer procfs$kmalloc()
 {
     InterruptDisabler disabler;
@@ -235,6 +301,7 @@ bool ProcFileSystem::initialize()
     addFile(createGeneratedFile("mounts", procfs$mounts));
     addFile(createGeneratedFile("kmalloc", procfs$kmalloc));
     addFile(createGeneratedFile("summary", procfs$summary));
+    addFile(createGeneratedFile("cpuinfo", procfs$cpuinfo));
     return true;
 }
 
diff --git a/Kernel/VirtualConsole.cpp b/Kernel/VirtualConsole.cpp
index 2f2c9b11a9..f4537fd766 100644
--- a/Kernel/VirtualConsole.cpp
+++ b/Kernel/VirtualConsole.cpp
@@ -23,7 +23,6 @@ VirtualConsole::VirtualConsole(unsigned index, InitialContents initial_contents)
 {
     s_consoles[index] = this;
     m_buffer = (byte*)kmalloc_eternal(80 * 25 * 2);
-    dbgprintf("VirtualConsole %u @ %p, m_buffer = %p\n", index, this, m_buffer);
     if (initial_contents == AdoptCurrentVGABuffer) {
         memcpy(m_buffer, s_vga_buffer, 80 * 25 * 2);
         auto vgaCursor = vga_get_cursor();
diff --git a/Kernel/i386.cpp b/Kernel/i386.cpp
index 9ebdd95c19..2554b1b352 100644
--- a/Kernel/i386.cpp
+++ b/Kernel/i386.cpp
@@ -447,4 +447,3 @@ void handleIRQ()
         s_irqHandler[irq]->handleIRQ();
     PIC::eoi(irq);
 }
-
diff --git a/Kernel/i386.h b/Kernel/i386.h
index f5634fe92b..e03c4a71b9 100644
--- a/Kernel/i386.h
+++ b/Kernel/i386.h
@@ -175,3 +175,16 @@ inline constexpr dword pageBaseOf(dword address)
     return address & 0xfffff000;
 }
 
+class CPUID {
+public:
+    CPUID(dword function) { asm volatile("cpuid" : "=a" (m_eax), "=b" (m_ebx), "=c" (m_ecx), "=d" (m_edx) : "a" (function), "c" (0)); }
+    dword eax() const { return m_eax; }
+    dword ebx() const { return m_ebx; }
+    dword ecx() const { return m_ecx; }
+    dword edx() const { return m_edx; }
+private:
+    dword m_eax { 0xffffffff };
+    dword m_ebx { 0xffffffff };
+    dword m_ecx { 0xffffffff };
+    dword m_edx { 0xffffffff };
+};