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]

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.

[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.