+#define leave_vx_info(s) __leave_vx_info(s,__FILE__,__LINE__)
+
+static inline void __leave_vx_info(struct vx_info_save *vxis,
+ const char *_file, int _line)
+{
+ vxlprintk(VXD_CBIT(xid, 5), "leave_vx_info(%p[#%d,%p]) %p[#%d,%p]",
+ vxis, vxis->xid, vxis->vxi, current,
+ current->xid, current->vx_info, _file, _line);
+ (void)xchg(¤t->vx_info, vxis->vxi);
+ current->xid = vxis->xid;
+}