系统调用混合映射关系的建模

混合映射关系指的是对于Windows APIa而言，它的对应实现不唯一，需视具体情况而定，不同情况下，与对应实现之间的映射关系也不尽相同，可以是前三种映射关系中的任何一种，也可以是前三种映射关系中两种或三种关系的组合。

定义23 对于函数序列Σ，若函数f属于函数序列Σ，即f∈∑，则用二元关系contain（Σ，f）来表示函数f与函数序列Σ之间的关系。

定义24 对于函数序列Σ，若函数序列∑＇属于函数序列Σ，即∑＇⊂∑，则同样用二元关系contain（∑，∑＇）来表示函数序列∑＇与函数序列Σ之间的关系。

定义25 （混合映射关系mixedMapping）对于函数f1，有n 种对应实现，组成函数序列Σ，其中有n1种对应实现是1：1 直接映射关系（fi∈∑，i=1…n1）；n2种对应实现是1：1 上下文相关映射关系（fj∈∑，j=1…n2）；n3种对应实现是1：n 上下文相关映射关系（），即其中n1 +n2 +n3 =n。函数序列中的函数有一定的先后执行顺序，假设函数序列中函数的执行顺序为：fk1→fk2→...→fkn，则函数f1与函数序列Σ之间的上下文相关映射关系可以表示为：

以Windows中的SetEvent函数为例，该函数的功能是创建一个有名（named）或无名（un-named）的事件对象。有名事件对象是用来在进程之间进行同步，Linux中的System V信号量实现了有名事件相同的功能；对于无名事件对象，Linux中的pthread 和POSIX都提供了相同功能。

如前文所述，若要创建一个System V信号量，首先需要调用函数semget，然后再调用函数semctl来完成对信号量数据结构的初始化。类似的，若要创建一个条件变量，首先需要调用phread 库中的函数pthread_cond_init，然后再调用函数pthread_condattr_init来对其进行初始化。然而若要创建的是一个POSIX信号量，则只需要调用函数sem_init即可。

CreateEvent函数执行后返回的是一个句柄，它有四个输入参数，其中lpEvent-Attributes是一个指针，它指向一个决定返回的这个句柄是否能够被继承的属性。如果该指针为NULL，那么说明该句柄不能被继承。bManualReset是一个标记，用来指定所创建的事件对象是手动复原还是自动复原。如果是TRUE，那么必须用ResetEvent函数来手动将事件的状态复原到无信号状态。如果设置为FALSE，当一个等待线程被释放以后，系统将会自动将事件状态复原为无信号状态。bInitialState指定事件对象的初始状态。如果为TRUE，初始状态为有信号状态；否则为无信号状态。lpName是指向事件对象名的指针，若该值为NULL，则将创建的是一个无名的事件对象。(www.xing528.com)

接下来用CreateEvent函数来创建一个最简单的无名事件对象：

则对应的POSIX信号量创建如下，其中sem_init函数的第三个参数是信号量计数值，用来设置信号量的初始状态，这里取值为0，意味着该信号量被初始化为无信号状态。

对应于创建条件变量的等效代码如下：

同样，对于Windows创建的有名对象，也有对应的Linux等效代码。例如再通过CreateEvent函数来创建一个最简单的有名事件对象，它与之前创建无名事件对象的区别在于，前者的最后一个参数为NULL，而后者的最后一个参数赋值为“myEvent”。

对应的创建System V信号量的等效代码如下：

从分析中可以看出，SetEvent函数有三个对应实现，其中一个1：1 直接映射关系，两个1：n 上下文相关映射关系，因此其对应实现的函数序列Σ={sem_init，Σ1，Σ2}，其中函数序列Σ1 中函数的执行次序为pthread_condattr_init→pthread_condattr_setpshared →pthread_cond_init→pthread_condattr_destroy；函数序列Σ2 中函数的执行次序为semget→semctl。根据定义25，函数SetEvent与其的对应实现之间的关系可以形式化表示为：