pt2_wirecount_dec
pt2_wirecount_dec(m, pte1_index(va));
pt2_wirecount_dec(mpte2, pte1_index(va));
pt2_wirecount_dec(mpte2, va >> PTE1_SHIFT);
pt2_wirecount_dec(mpt2pg, pte1_index(va));