newbie questions

[Norman Feske]

Hi Ross,

> I'm very happy/relieved to here this :)  (As a suggestion -although
> from an amateur- perhaps you should specifically mention that
> ACL's/unix file permissions are not intrinsic to genode nor are they
> planned to be.  Because on first pass reading I go the impression
> that the file permissions might be planned although it is a cap based
> system-- and I was reading it from the perspective of someone
> familiar with cap theory and knows the difference between caps and
> ACLs.  I feel that if someone who read this wasn't already familiar
> cap OSes and all they knew were traditional ACL systems then they
> would assume that the file permissions are indeed already present and
> necessarily intrinsic.)

You are right, the section "Successive policy management" may be
misleading. I just wanted to use Unix file permissions as an example,
but certainly, it is better to avoid this reference. I will try to
find a more general example.

> Thanks once again for answering, but if you don't mind can I bother
> you with just few more last questions:
> A: Two questions regarding the interfaces between parent and child-
> 1) How does a server to signal to the client that it will need/does
> need more quota.  (The interface methods given in the "Interfaces and
> Mechanisms" document allows a client to give quota to a server, but
> hows does the client know when and how much it needs to give?)

That is a very good point. At present, the resource requirements of the
currently implemented services are pretty static. We use to transfer
quota at session-creation time and do not (yet) need to use a subsequent
'tranfer_quota' call at all. But how does a client know, how much quota
to donate? This information is actually provided as a part of the
service's interface definition in the form of a 'Connection' class that
comes along with the server's RPC-interface classes. For example, the
Nitpicker GUI server requires the client to donate a memory quota
dependent on the size of the pixel buffer to use. The corresponding
'Connection' class is located at

  os/include/nitpicker_session/connection.h

and encapsules the heuristics about how much resources are to be donated
when creating a session with a certain buffer size. Thereby, the
application programmer does not need to care about that. He just opens a
session to Nitpicker by constructing a 'Nitpicker::Connection' object

  static Nitpicker::Connection nitpicker(width, height);

and interacts with the server via member functions of the created
object, for example

  nitpicker.refresh();

However, the service discovery and resource negotiation are still
subject for improvement in the future.

> 2)Are the session request strings expected to follow a format and naming standard for common types of services?

The arguments are service specific. The only naming standard is the
use of a comma-separated list of <tag>=<value> pairs and the character
set to be used for tags and values. However, the meaning of tags
depends on each server - very much like command line arguments of
Unix programs depend on the actual program. There are some arguments
that are interpreted by the parent and should be used in the
intended way, for example 'ram_quota' specifies the memory quota, the
child is going to donate to the server, or 'label' holds an optional
textual label for the session. But in general, these arguments are
optional and regarded as untrusted by the parent. However, in order
to implement a least-priviledge policy in the parent, the parent will
have to know the services and their arguments and filter session
arguments according to the policy.

> B:Other questions-
> 1)Do you eventually intend to formally verify the software? (I
> believe the NICTA /OK-labs L4 kernel that genode can target is in the
> process of being verified and was wondering if you will likewise wish
> to verify genode to supply a fully mathematically verified framework
> for building OS personalities on).

Currently, we do not pursue such plans. The seL4 verification project
by OK-Labs/NICTA is exciting but it also shows the tremendous amount of
effort and expertise that is needed for such a project. Actually, the
complexity of the Genode framework is in the same range as the code used
in the seL4 project, which allows a rough estimation of the feasibility
and costs of verifying the framework's code. However, in contrast to
seL4, the Genode framework is multithreaded. As far as I know, multi-
threading is not addressed by the seL4 project (and I suppose, this is
for a good reason).

> Lastly, I re-read the "Interfaces and Mechanisms" and I think I've
> found another minor error- in the section "Quota" in the sentence "Once,
> the server requests to close the session, the child is responsible to
> release all resources that were used for this session.". Aren't the
> words "server" and "child" meant to be swaped around here?

Technically, "child" is correct because the server is actually a child
but I clearly see your point. ;-) Thanks for the hint - I am going to
change the wording to be less confusing.

Best regards
Norman