小编Bra*_*ing的帖子

在Agda中,a的类型forall以这样的方式确定:以下都具有类型Set1(where Set1的类型Set和A类型Set):

Set ? A
A ? Set
Set ? Set

但是,以下类型Set:

A ? A

我明白,如果Set有类型Set,就会有矛盾,但我没有看到,如果上述三个术语中的任何一个有类型Set,我们就会有矛盾.那些可以用来证明是假的吗？它们可以用来表明Set : Set吗？

在Linux内核以及在线的许多x86教程中,我看到人们建议使用两个代码段和两个数据段.我理解需要两个代码段,因为CPL需要与DPL完全匹配(对于不符合的段).

但是,这些教程中没有一个(也没有任何关于StackOverflow的相关问题),具体说明为什么我们需要两个数据段.这些工作与代码段不同,因为CPL = 0的进程可以访问DPL = 3的数据段.

如果我们在不同权限级别的进程之间切换,则具有两个数据段的缺点是必须重新加载DS,ES等寄存器.

所以我的具体问题是:鉴于我们使用的是平面内存模型,所有代码和段完全重叠,它的用途和内核数据段的用途是什么,而不仅仅是一个用户数据段？