#include <amd64/regsasm.h>

.global do_sched1
do_sched1:
  movq %rdi, %rsp
  movq %rsi, %cr3
  pop_regs
  addq $16, %rsp
  iretq