日志生成时间 20:19  2007-7-11

实习单位：中国科学院计算技术研究所智能中心操作系统组
导师：马老师

上午8:00到达ict大楼，开始了实习的第一天。

我被分配到马老师旁边的位子上，这下我就可以随时和他交流了,Hoho~
稍后，我们到会议室聊了会儿，主要是确认了我的实习时间，然后仔细介绍了他当前想做或正在做的几个项目：

·龙芯原型机的初始化代码重构
·SMP机虚拟多操作系统，多种操作系统底层代码重构
·多处理机通信协议正确性的形式化证明
·Google文件系统研究

我一五一十地跟他说了我的实习计划：看分数！能保研，就长些，不能，我就要早些回去准备考研了。很直接，不过这样也好，先说明了，免得以后要走却不好开口。
关于选题，现在看来我犯了一个毛病，而且是一个老毛病：我略加思考就决定选第一个。
我有个不大好的习惯：遇到一个问题时总趋向于立即找到一个基本解决思路—实际上我们现在遇到的很多问题是不可能马上能够得出大体解决方案的。最终方案的得出需要很多基础知识做支撑，这些知识是需要时间去学习的。

关于第一个题目，里面涉及到了大量的知识产权相关的内容，很多内容都不能写入实习报告，这给实习报告的撰写可能会带来很大的困难。束缚太多！马老师让我先熟悉下再做决定，要做也可以，最终报告让他审阅下就行。这一周熟悉课题，下周选择一个深入学习。

然后，他给我分配了一个帐号，让我看了两份介绍软硬件环境的说明。

计算所里现在都是用桌面终端方式来使用计算机资源，每个人桌上只要一个终端和一台显示器就可以了，通过网络连接到资源服务器上。
这种方式有利于权限和信息的管理，并且降低了软硬件成本。唯一缺点就是网络负载大，终端上的刷新操作有些延迟。

上午，我开始为选题做准备，从形式化证明开始，搜集了很多软件测试，协议测试方面的资料了解，以期获得一个大致概念。其中比较有参考价值的是清华的一篇毕业论文《PPP协议测试》，他们利用清华的PITS系统对PPP协议实现进行了一致性测试。不过现在我感觉，这个跟形式化证明还不是一个概念。

中午，和叶子一起在中科院楼下的餐厅吃饭。真贵！

中间只有一小时的时间。1点回到实验室，实在熬不住，趴了……13:50醒来一看，咦，原来大家都趴了*^_^*。原来，所谓一点要到实验室指的是“来”，而不是来工作。我还以为北京的民工都不午休……

下午继续看形式化内容，稍微有点小感觉了，心也沉下去了。把马老师博士毕业论文中提到的一个叫Spin的测试工具下了一个，看了两个例子，没有文档，自己摸索着编了两个测试程序，还挺有意思。这个软件可以模拟多道程序并行执行，每次执行的结果可以都不一样。论文中还用到了一种叫做PROMELA的形式化描述语言，用来描述论文中设计的通信协议。没文档，好复杂，尽管沉着心，最终还是晕塌了%&#￥……@

下午同时关注了下龙芯方面的东西，网上资料少，没深入。

下午六点的时候整层实验室人都基本走完了，马老师还在，看了下我的工作进度，我也问了他一些问题。
当我问到他的论文中PROMELA和Spin之间的关系的时候他笑着十分坦白地告诉我那是当初为了凑字数，硬凑上去的，后来答辩的时候导师问他是如何利用Spin来证明协议正确性的，他也傻眼了。呵呵，这个老师真可爱！

他又把我介绍给了另外一个老师，说了下给我的备选课题。那个老师否认了第一课题，说那个已经没有什么价值，对于第二个他予以了充分的肯定，觉得那个的确需要重构。不过他担心我时间不够，可能刚刚进入角色就要走人了。的确，我更担心……马老师说没关系，至少可以写个分析报告出来，作为实习成果。呵呵，真是好老师，处处还是为着学生想的。我要努力，能走多远，尽量走多远。

 

PS：有周末，hoho~可以溜达溜达咯
PS2: 有高温假，7-23 ~ 8-2 ，我可以自由选择。由于我可能要回来复习考研，那段日子我故要就得在所里单干了。Fighting~