lazy Scheduling Context rebind + improve tool <-> monitor ABI

[dreamliner787-9]

Applied seL4/seL4#523 to workaround seL4/seL4#1617, and improved tool <-> monitor ABI by creating a metadata struct per PD, rather than adding a new symbol for every type of metadata.

[Indanz]

First, this really should be two separate commits, not lumped together like this.

Secondly, I'm missing creating a notifications object for passive servers that don't otherwise have one already, and binding the SC to the notification object if the PD is passive.

That last thing is really the only change you need compared to active PDs for setup.

Only other change needed is that you bind the SC when restarting the task, but I don't think Microkit does that yet, but rust-sel4 does I think.

[Indanz]

There is no need to do this resume and you can bind the SC to the notification when you create the notification for a passive thread. This feels like the wrong place for that.

[dreamliner787-9]

There is no need to do this resume

I think this ties in to my reply below.

and you can bind the SC to the notification when you create the notification for a passive thread. This feels like the wrong place for that.

We did consider binding the PD's Notification to the SC in the initialiser by adding a passive: bool to the TCB spec object. But we felt like the initialiser should not be concerned with this detail.

[Indanz]

We did consider binding the PD's Notification to the SC in the initialiser by adding a passive: bool to the TCB spec object. But we felt like the initialiser should not be concerned with this detail.

But this is init code, of course it belongs in the initialiser. These details are exactly the kind of things it should be concerned about. And if you do it in the loader, you also automatically fix any race because you can do the operations in the correct order. Now you add subtle ad hoc code to work around the ordering problem, without being explicit about it. That's a bad sign.

You already have pd.passive property anyway, passing that info to the loader only seems prudent.

[Indanz]

Why?

[dreamliner787-9]

Hi Indan, we intended for passive PDs to be resumed by the monitor, because we don't want them to start processing events before being converted to passive. Which can happen on multi-core.

[Indanz]

There isn't any race condition, other than a harmless corner case of possibly handling the very first IPC call with the NF's SC instead of the caller's SC.

But that's only true if the TCB is running while you bind SC's. Normally you would do that only after setup. That is, if you do the seL4_TCB_WriteRegisters with resume == true after the SC and NF binding, there is no race.

[dreamliner787-9]

First, this really should be two separate commits, not lumped together like this.

Yes I agree, will split them up.

Secondly, I'm missing creating a notifications object for passive servers that don't otherwise have one already, and binding the SC to the notification object if the PD is passive.

All PDs have a notification object in their capDL spec so they will be created automatically by the initialiser.

microkit/tool/microkit/src/capdl/builder.rs

Lines 710 to 736 in da0ca91

	// Step 3-7 Create endpoint object for the PD if it has children or can receive PPCs, else it will be a notification
	let pd_ntfn_obj_id = capdl_util_make_ntfn_obj(&mut spec_container, &pd.name);
	let pd_ntfn_cap = capdl_util_make_ntfn_cap(pd_ntfn_obj_id, true, true, 0);
	let mut pd_ep_obj_id: Option<ObjectId> = None;
	pd_id_to_ntfn_id.insert(pd_global_idx, pd_ntfn_obj_id);
	if pd.needs_ep(pd_global_idx, &system.channels) {
	pd_ep_obj_id = Some(capdl_util_make_endpoint_obj(
	&mut spec_container,
	&pd.name,
	false,
	));
	let pd_ep_cap =
	capdl_util_make_endpoint_cap(pd_ep_obj_id.unwrap(), true, true, true, 0);
	pd_id_to_ep_id.insert(pd_global_idx, pd_ep_obj_id.unwrap());
	caps_to_insert_to_pd_cspace
	.push(capdl_util_make_cte(PD_INPUT_CAP_IDX as u32, pd_ep_cap));
	} else {
	let pd_ntfn_cap_clone = pd_ntfn_cap.clone();
	caps_to_insert_to_pd_cspace.push(capdl_util_make_cte(
	PD_INPUT_CAP_IDX as u32,
	pd_ntfn_cap_clone,
	));
	}
	caps_to_bind_to_tcb.push(capdl_util_make_cte(
	TcbBoundSlot::BoundNotification as u32,
	pd_ntfn_cap,
	));

Only other change needed is that you bind the SC when restarting the task, but I don't think Microkit does that yet, but rust-sel4 does I think.

Yes, the capDL initialiser configure SCs and bind them to TCBs for us, so we only need to bind Notification to SC for passive PDs.