diff options
| -rw-r--r-- | dsl.mdwn | 22 | ||||
| -rw-r--r-- | idl.mdwn | 11 | ||||
| -rw-r--r-- | open_issues/code_analysis.mdwn | 8 | ||||
| -rw-r--r-- | open_issues/formal_verification.mdwn | 16 | ||||
| -rw-r--r-- | open_issues/performance.mdwn | 19 | ||||
| -rw-r--r-- | open_issues/profiling.mdwn | 4 |
6 files changed, 72 insertions, 8 deletions
diff --git a/dsl.mdwn b/dsl.mdwn new file mode 100644 index 00000000..28f70d7d --- /dev/null +++ b/dsl.mdwn @@ -0,0 +1,22 @@ +[[!meta copyright="Copyright © 2010 Free Software Foundation, Inc."]] + +[[!meta license="""[[!toggle id="license" text="GFDL 1.2+"]][[!toggleable +id="license" text="Permission is granted to copy, distribute and/or modify this +document under the terms of the GNU Free Documentation License, Version 1.2 or +any later version published by the Free Software Foundation; with no Invariant +Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license +is included in the section entitled [[GNU Free Documentation +License|/fdl]]."]]"""]] + +[[!meta title="DSL"]] + +A *DSL* is a *domain-specific language* ([[!wikipedia Domain-specific_language +desc="Wikipedia article"]]). + +Compared to general-purpose programming languages, these are a candidate for +[[open_issues/formal_verification]]. + +DSLs are frequently used as [[IDL]]s for implementing [[RPC]] systems, but can +also used for other portions of the [[kernel]], such as [[capability]] systems. +This is exemplified for [[microkernel/Barrelfish]] in +{{$microkernel/barrelfish#fof_plos09}}, for example. @@ -9,11 +9,16 @@ Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license is included in the section entitled [[GNU Free Documentation License|/fdl]]."]]"""]] -An *IDL* is an *interface definition language*. The most well-known is CORBA. +[[!meta title="IDL"]] + +An *IDL* is an *interface definition language* ([[!wikipedia +Interface_description_language desc="Wikipedia article"]]). A well-known one +is CORBA. These are [[DSL]]s. An IDL compiler takes a specification and generates stub code that hides the transport details, and by this implements a [[RPC]] system. In the case of [[Mach's MIG|microkernel/mach/mig]], this hides the marshalling -and unmarshalling of parameters according to [[microkernel/Mach]]'s semantics, -and invoking the respective [[microkernel/mach/port]] operations. +and unmarshalling of procedures' parameters to and from +[[microkernel/mach/message]] format, according to [[microkernel/Mach]]'s +semantics, and invoking the respective [[microkernel/mach/port]] operations. diff --git a/open_issues/code_analysis.mdwn b/open_issues/code_analysis.mdwn index 114dfbbf..ad59f962 100644 --- a/open_issues/code_analysis.mdwn +++ b/open_issues/code_analysis.mdwn @@ -8,7 +8,13 @@ Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license is included in the section entitled [[GNU Free Documentation License|/fdl]]."]]"""]] -There is static and dynamic code analysis. This overlaps with [[debugging]]. +In the topic of *code analysis* or *program analysis* ([[!wikipedia +Program_analysis_(computer_science) desc="Wikipedia article"]]), there is +static code analysis ([[!wikipedia Static_code_analysis desc="Wikipedia +article"]]) and dynamic program analysis ([[!wikipedia Dynamic_program_analysis +desc="Wikipedia article"]]). This topic overlaps with [[performance +analysis|performance]], [[formal_verification]], as well as general +[[debugging]]. * [[GCC]]'s warnings. Yes, really. diff --git a/open_issues/formal_verification.mdwn b/open_issues/formal_verification.mdwn new file mode 100644 index 00000000..168d59a4 --- /dev/null +++ b/open_issues/formal_verification.mdwn @@ -0,0 +1,16 @@ +[[!meta copyright="Copyright © 2010 Free Software Foundation, Inc."]] + +[[!meta license="""[[!toggle id="license" text="GFDL 1.2+"]][[!toggleable +id="license" text="Permission is granted to copy, distribute and/or modify this +document under the terms of the GNU Free Documentation License, Version 1.2 or +any later version published by the Free Software Foundation; with no Invariant +Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license +is included in the section entitled [[GNU Free Documentation +License|/fdl]]."]]"""]] + +*Formal verification* ([[!wikipedia Formal_verification desc="Wikipedia +article"]]) deals with formally reasoning about a program's correctness. + +Especially in the field of [[DSL]]s, this is used for asserting program codes' +correctness, as explained in {{$microkernel/barrelfish#fof_plos09}}, for +example. diff --git a/open_issues/performance.mdwn b/open_issues/performance.mdwn index 3b4c4537..9b3701b3 100644 --- a/open_issues/performance.mdwn +++ b/open_issues/performance.mdwn @@ -8,10 +8,21 @@ Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license is included in the section entitled [[GNU Free Documentation License|/fdl]]."]]"""]] - * general [[RPC]] overhead +*Performance analysis* ([[!wikipedia Performance_analysis desc="Wikipedia +article"]]) deals with analyzing how computing resources are used for +completing a specified task. - * [[I/O System|io_system]] +[[Profiling]] is one relevant tool. - * [[fork]] +In [[microkernel]]-based systems, there is generally a considerable [[RPC]] +overhead. - * [[unit testing]] +In a multi-server system, it is non-trivial to implement a high-performance +[[I/O System|io_system]]. + +When providing [[faq/POSIX_compatibility]] (and similar interfaces) in an +environemnt that doesn't natively implement these interfaces, there may be a +severe performance degradation. For example, in this [[`fork` system +call|/glibc/fork]]'s case. + +[[Unit_testing]] can be used for tracking performance regressions. diff --git a/open_issues/profiling.mdwn b/open_issues/profiling.mdwn index 3f9330ba..f56ae974 100644 --- a/open_issues/profiling.mdwn +++ b/open_issues/profiling.mdwn @@ -8,6 +8,10 @@ Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license is included in the section entitled [[GNU Free Documentation License|/fdl]]."]]"""]] +*Profiling* ([[!wikipedia Profiling_(computer_programming) desc="Wikipedia +article"]]) is a tool for tracing where CPU time is spent. This is usually +done for [[performance analysis|performance]] reasons. + * [[gprof]] Should be working, but some issues have been reported, regarding GCC spec |