عن العمل في المملكة المتحدة

في هذه المقالة أطرح بعض أشهر أنواع التأشيرات التي تتيح العمل والهجرة إلى المملكة المتحدة. تستهدف تلك المقالة العمال العرب الماهرين من خريجي الجامعات.

العمل بدوام كامل في المملكة المتحدة يستلزم (في الغالب) نوع من الكفالة تسمى sponsorship [0]، وهي أن تتكفل شركة أو مؤسسة ما بالعمال الأجانب. تلك الكفالة تتضمن دفع بعض المصاريف لإصدار شهادة، وإعلام الـ Home Office. يحدد لكل شركة عدد معين من العمال الأجانب الذي يمكن إحضارهم. ويجب على الشركة أن تثبت أنه لا يوجد عمال بريطانيين قدموا على نفس الوظيفة ومؤهلين مثل العمال الأجانب. ولذلك، معظم الشركات (خاصة المتوسطة والصغيرة) تجد صعوبة في احضار العمال الأجانب ودعمهم. ولكن هناك أيضا بعض التأشيرات التي تتيح العمل بدون كفالة، أسرد بعضها لاحقا. 

تأشيرة الخريجين

تتيح المملكة المتحدة نوع من التأشيرات [1]  للخريجين من جامعاتها. تختلف المدة حسب نوع الدراسة، فخريجي البكالوريوس والماجستير يحصلون على عامين، أما خريجي الدكتوراة فثلاثة أعوام. يجب التقديم على التأشيرة بعد إثبات التخرج من الجامعة وأثناء وجودك في المملكة المتحدة. تتيح تلك التأشيرة العمل (أو البحث عنه) بدون كفالة. بعد انقضاء تلك المدة، يجب الحصول على نوع آخر من التأشيرات للاستمرار في المكوث في المملكة المتحدة، مثل تأشيرة العمل مثلا. 

تأشيرة العمل

تعتبر أشهر نوع من التأشيرات للعمل [2] في المملكة المتحدة. تستلزم تلك التأشيرة الحصول على عقد عمل من جهة بالمملكة المتحدة على استعداد بالكفالة. كما ذكرت سابقا، يجب على الشركة أن تثبت أنه لا يوجد عمال بريطانيين قدموا على نفس الوظيفة ومؤهلين مثل العمال الأجانب. إذا ترك العامل جهة العمل المتكفلة به، فيجب أن يجد جهة أخرى تكفله خلال شهرين، وإلا يجب عليه ترك المملكة المتحدة.

العاملين بالقطاع الطبي

يوجد تأشيرة للعاملين بالقطاع الطبي من الأطباء والممرضين والمتكفلين بكبار السن [3]. يستلزم العمل مع القطاع الصحي بالمملكة المتحدة NHS أو ما له علاقة به، ويستلزم الحصول على كفالة من جهة ما وإثبات اتقان اللغة الانجليزية.

تأشيرة المتميزين

يوجد نوع خاص من التأشيرات للمتميزين [4] في مجالاتهم لجذبهم إلى المملكة المتحدة. فمثلا الحاصلين على الدكتوراة والجوائز العلمية والبحثية، أصحاب براءات الاختراع، العاملين المتميزين في قطاع الحاسبات والبرمجيات والفنون، إلخ. تستلزم تلك التأشيرة إثبات التميز وبعض الخطط التي توضح كيف سيفيد الفرد اقتصاد المملكة المتحدة، وتقديم 3 جوابات توصية على الأقل من أشخاص رواد في مجالاتهم. لا تستلزم تلك التأشيرة الحصول على الكفالة للعمل، ويمكن المكوث في المملكة المتحدة وتجديد تلك التأشيرة بسهولة.

الإقامة الدائمة (الهجرة)

يمكن الحصول على الإقامة الدائمة [5] بطرق مختلفة. تتراوح المدة التي يمكن تقديم الفرد بعدها على اقامة دائمة من 3 إلى 5 سنوات. فمثلا، يمكن لشخص يعمل بتأشيرة عمل التقديم بعد 5 سنوات على الهجرة الدائمة. بعدها لا يستلزم الحصول على الكفالة للعمل أو المكوث في المملكة المتحدة.

بخلاف ذلك، يوجد بعض التأشيرات التي تتيح العمل مثل اللجوء ولم الشمل و تأشيرات لعائلات العاملين من من معهم بعض التأشيرات السابق ذكرها (أزواج/زوجات) العاملين في المملكة المتحدة، يمكن القراءة عنها من الموقع الحكومي [5]. ملاحظة، تتغير قوانين الهجرة سريعا في المملكة المتحدة.

المصادر

[0] https://www.gov.uk/uk-visa-sponsorship-employers

[1] https://www.gov.uk/graduate-visa

[2] https://www.gov.uk/skilled-worker-visa

[3] https://www.gov.uk/health-care-worker-visa

[4] https://www.gov.uk/global-talent

[5] https://www.gov.uk/browse/visas-immigration/settle-in-the-uk

[6] https://www.gov.uk/browse/visas-immigration

عن الدراسة في المملكة المتحدة

 

مقدمة

في هذه المقالة ألخص خبرتي في الدراسة في المملكة المتحدة وأعطي بعض النصائح والآراء للراغبين في الدراسة هناك. هذه النصائح قائمة على خبرتي بدراسة الماجستير في جامعة يورك والدكتوراة بجامعة كامبريدج بإنجلترا، والعمل هناك بعد ذلك.

المقالة تستهدف الطلاب العرب الراغبين في السفر لدراسة الماجستير والدكتوراة بشكل كبير وإن كانت بعض النصائح تنطبق أيضا على الراغبين في دراسة البكالوريوس. 

نظام التعليم في المملكة المتحدة

المملكة المتحدة بها جامعات من الأفضل والأقدم في العالم [1، 2]  مثل كامبريدج وأوكسفورد. الدراسة في المملكة المتحدة ليست مجانية، ومصاريفها باهظة حيث تعتبر مصدر أساسي للدخل القومي للبلاد. تختلف قيمة المصاريف بين الطلاب البريطانيين والطلاب من خارج البلاد، وفي الغالب تكون المصاريف مضاعفة للطلاب غير البريطانيين مقارنة بالبريطانيين.

البكالوريوس

مدة البكالوريوس في بريطانيا 3  سنوات في الغالب. ويتطلب امتحان يسمى GCE للالتحاق بالجامعة أولا.  في بعض التخصصات مثل علوم الحاسب والهندسة، يمكن الحصول على البكالوريوس والماجستير معا خلال 4 سنوات فقط.

الماجستير

تتراوح مدة دراسة الماجستير ما بين سنة إلى سنتين حسب التخصص. معظم برامج الماجستير تنقسم إلى دراسة مواد نظرية والامتحان عليها، ورسالة ماجستير بحثية أو عملية. يوجد أيضا في بعض التخصصات ماجستير بحثي فقط حيث لا يدرس فيه الطلاب مواد ولا يوجد امتحان، التقييم يكون فقط على رسالة ماجستير بحثية، وتعتبر برنامج مصغر من الدكتوراة.

الدكتوراة

تتراوح مدة دراسة الدكتوراة من ٣  إلى ٤ سنوات في المتوسط، على خلاف الولايات المتحدة حيث أن ٥ أعوام هو المتوسط. في الغالب لا يوجد متطلبات لدراسة مواد بعينها والامتحان عليها. ولكن معظم الجامعات توفر ورش عمل ومحاضرات تساعد الطلاب على وترشدهم إلى أساليب وأدوات البحث العلمي، كيفية استخدام اللغة الانجليزية في البحث العلمي، كيفية كتابة رسائل وأبحاث، وما إلى ذلك. التقييم قائم فقط على رسالة الدكتوراة في نهاية المدة.

اختيار الجامعات

يوجد أكثر من ١٦٠ جامعة في المملكة المتحدة. يوجد ما يسمى بمجموعة الـ Russell Group وتضم أفضل الجامعات في البلاد، وتلك الجامعات تنافس في الترتيب العالمي أيضا. اختيار الجامعات يعتمد على امكانيات المتقدم، فكلما ارتفع ترتيب الجامعة، كلما صعبت المتطلبات والتنافس على مقاعد الالتحاق بالدراسة. مثلا، في جامعة كامبريدج في عام 2022، كانت نسبة القبول في الجامعة ككل 19% [3] في برامج البكالوريوس. هذا على غرار جامعة يورك مثلا وهي أقل في الترتيب، ونسبة القبول بها كانت 83.8% في عام 2017 [4].

عند اختيار الجامعة، يوجد بعض المعايير التي تختلف من شخص لآخر وبين التخصصات والأولويات، اسرد أكثرهم استخداما في الفقرة التالية.

•  بناء على ترتيب الجامعة

لزيادة فرص القبول في جامعة أو أكثر، أنصح بالتقديم في جامعة من ضمن ال١٠ الأفضل، ثم جامعة من ال١٠ إلى ٢٠ الأفضل وهكذا. كما أرشح التقديم على ٣ او ٤ جامعات بحد أقصى.

• بناء على التخصص

يوجد بعض الجامعات ليس بها بعض التخصصات، فالأولى هو اختيار الجامعات التي بها تخصصك أولا، ثم ترتيبهم بناء على مستوى الجامعة ومستواك. 

• بناء على المدينة

تختلف تكلفة المعيشة من مدينة إلى آخرى. فمثلا تعتبر لندن أغلى مدينة للمعيشة مقارنة بمدن الشمال. بالمثل، هناك بعض المدن التي بها جاليات عربية كبيرة مثل لندن، برمنجهام، ليدز، برادفورد، إلخ، مقارنة بمدن أخرى صغيرة.

• بناء على بحثك

معظم الجامعات توفر كافة المعلومات اللازمة عن الجامعة، السكن، المعيشة، التكلفة، الأنشطة، التخصص والمواد، إلخ. من أهم النقاط هو عمل واجبك في دراسة موقع الجامعة والتخصص جيدا جدا، مثلا مواد التخصص وكيفية التقييم، وجود غرف للصلاة أم لا، وجود رياضات ونوادي ونشاطات تهتم بها أو لا. أدرس موقع الجامعة والتخصص أولا قبل طرح اسئلتك على الغير، ففي الغالب الجواب هناك.

• أدوات البحث

يوجد بعض المواقع ومحركات التي تساعد على اختيار الجامعات بناء على البرنامج (ماجستير، دكتوراة، إلخ)، التخصصات، والمنح. أرشح استخدام مواقع بس Find a Master أو Find a PhD مثلا، ثم ترتيبهم.

ميعاد التقديم

بالنسبة للبكالوريوس والماجستير، يفضل البدء في التحضير قبل عام على الأقل. مثلا، للالتحاق ببرنامج ماجستير يبدأ في أكتوبر ٢٠٢٤، يجب البدء بالتحضير والتقديم في أكتوبر ٢٠٢٣. بعض الجامعات والمنح لها مواعيد محددة للتقديم تغلق بعد ذلك. 

أما بالنسبة للدكتوراة، فيفضل (بناء على نصيحتي اللاحقة) البدء قبل ذلك أيضا من حيث قراءة الأبحاث والتواصل مع المشرفين المحتملين، قبل البدء الرسمي في التقديم على الجامعة.

الملخص، ابدأ بالتحضير مبكرا.

شروط التقديم

اللغة

تختلف شروط التقديم من جامعة لأخرى وباختلاف التخصصات. ولكن جميعهم يطلبون اجتياز امتحان اللغة الانجليزية (IELTS or TOEFL) بدرجة معينة (كل جامعة تحدد درجة الاجتياز). يوجد أيضا بعض الجامعات التي تتيح دراسة اللغة الإنجليزية لعدة أشهر قبل البدء بدراسة التخصص، كبديل لاجتياز اللغة الانجليزية. في الغالب يمكن التقديم على الجامعة بدون امتحان اللغة، وفي حال قبولك، سيكون القبول مشروط على اجتياز امتحان اللغة. وكما ذكر سابقا، كلما زاد ترتيب الجامعة، كلما اشترطت درجة أعلى في اللغة. فمثلا تخصص علوم الحاسب بكامبريدج يتطلب 7.5 في امتحان IELTS و7 على الأقل في ال4 أقسام الامتحان [5]. أما يورك فتتطلب درجة 6 و 5.5 على الأقل في ال4 أقسام [6]. وجب الذكر أن معظم جامعات المملكة المتحدة لا تتطلب امتحانات GRE مثل الولايات المتحدة.

التكلفة

تنقسم التكلفة إلى جزئين أساسيين: مصاريف الجامعة، وتكاليف المعيشة. تختلف تكلفة ومصاريف الدراسة بشكل كبير على الجامعة والتخصص، ارجع إلى موقع الجامعة والتخصص لمعرفة التكلفة. أثناء التقديم على الجامعة، يجب أن تحدد إذا كنت ستتكفل بمصاريف الجامعة من مالك الخاص، أو عن طريق منحة. يجب أيضا الأخذ في الحسبان مدة الدراسة والمدينة، حيث ستطلب منك إثباتات (بيان بنكي كمثال) قدرتك على تحمل نفقات المعيشة وهي تختلف من مدينة إلى أخرى. فمثلا (أثناء كتابة هذه المقالة في عام 2023)، تقترح الحكومة مبلغ 1334 جنيه استرليني شهريا للدارسين في لندن، و1023 جنيه استرليني للمدن الأخرى [7]. يوجد أيضا موقع يحدد في المتوسط تكلفة المعيشة بناء على المدينة، والمقارنة بمدن أخرى [8].

شهادات التخرج السابقة

في حال التقديم على الماجستير أو الدكتوراة، تطلب الجامعة شهادات التخرج بتفصيل المواد ودرجاتها باللغة الانجليزية. بعض الجامعات والتخصصات تحدد حد أدنى لتقدير التخرج أيضا. على خلاف الجامعات العربية، بعض الجامعات تسمح بالتقديم على الدكتوراة بدون شهادة ماجستير أيضا، ولكن بعضهم يتطلبها. 

المنح

المنح من أهم النقاط عند الغالبية حيث أن الدراسة في المملكة المتحدة مكلفة جدا. هناك عدة أنواع من المنح، فيمكن أن تحصل على منحة جزئية أو كاملة (مصاريف الدراسة بالإضافة إلى تكاليف المعيشة). بالنسبة للبكالوريوس والماجستير، فإن المنح قليلة وتنافسية جدا مقارنة بالدكتوراة. يوجد مصادر عديدة للمنح مثل البعثات الحكومية من بلدك، منح من منظمات أو بنوك عربية واسلامية، تعاون بين المملكة المتحدة وبعض البلاد، أو من الجامعة والقسم نفسهم، إلخ. بعض أشهر المنح (التي أعرفها) كالآتي:

• [مصر] مشرفة نيوتن [14]

• [مصر] مؤسسة القلعة [15]

• [بعض البلاد العربية] منظمة سعيد [16]

• [كل البلاد العربية] تشيفننج [17]

• [للمسلمين] منح البنك الإسلامي [18]

كما يوجد بعض المنح لدعم الأقليات وتشجيع النساء على الدراسة في مجالات العلوم والهندسة مثلا [9]. خلاف ذلك يوجد موقع Find a PhD ومن خلاله يمكن البحث عن المنح في التخصصات المختلفة من مصادر عدة. فمثلا للبحث عن المنح في علوم الحاسب في المملكة المتحدة، أدخل هنا [10].

نصائح للتقديم على الدكتوراة

في رأيي الخاص، تعتبر دراسة الدكتوراة عمل منخفض الأجر. ففي غالبية برامج الدكتوراة يفيد الطالب القسم والجامعة بنشر الأبحاث والعمل على المشاريع الممولة. لا أنصح بالقدوم على دراسة الدكتوراة بغير منحة، على الأقل جزئية.

عند أخذ خطوات التقديم على الدكتوراة، يجب أن تدرس موقع القسم والجامعة جيدا أولا. فمثلا، تصفح الأساتذة العاملين هناك، الموضوعات البحثية، المشاريع، وفرص المنح. إذا كنت تعتقد أن هذا البرنامج الدراسي مناسب لك، يمكن أن تأخذ الخطوة ا لتالية.

يوجد الكثير ممن يريدون الالتحاق بالبرنامج الدراسي، خاصة إذا كان من جامعة مرموقة وبها منح. فأنت تنافس مئات أو آلاف من جميع دول العالم. ما الذي يجعلك تتميز إذا كنت فقط قدمت بشهادة تخرجك أو راسلت مشرف محتمل سائلا عن فرصة للعمل معه؟! يوجد بعض النصائح كالآتي.

أولا، اقرأ وأدرس ولخص أبحاث القسم وبالأخص المتعلقة بالمشرف المحتمل الذي تود العمل معه، وادرس مشاريعه. بعد ذلك، إذا كنت تعتقد أنك تستطيع أن تطور أو تبني على تلك الأبحاث، فراسله بمعلومات تقنية ومقترح بحثي، واذكر انك مهتم بدراسة الدكتوراة معاه. لا تجعل الرسالة نفسها طويلة. أو فقط إذا كان عندك بعض الأسئلة التقنية في أبحاثهم ومشاريعهم، فاسألهم. الملخص، أثبت لهم أنك جدي بالأمر بدراسة أعمالهم البحثية ومشاريعهم وإثبات قدرتك على الفهم والتحصيل ويفضل التطوير في ذلك المجال. 

في بعض التخصصات مثل علوم الحاسب والهندسة، ينشر القسم مشروعات مفتوحة المصدر من الممكن لأي أحد دراستها والعمل عليها إذا استطاع (وإذا كانت مشاركتهم لها قيمة).

إذا كان لديك بعض الوقت بعد ذلك، فمن الممكن أن تنشر بحث علمي أو survey متعلقة بأبحاثهم ومشاريعهم، ويمكن أن تراسلهم طالبا آرائهم في البحث أو حتى التعاون معهم واضافتهم عليه. من رأيي هذه أفضل وسيلة لزيادة فرص القبول والرد من مشرف الدكتوراة والمنح أيضا.

أخيرا، إذا كان لديك فرصة للذهاب إلى الجامعة والقسم ومقابلة أساتذتهم، أو حتى اقتراح إعطاء محاضرة عن خبرتك في المجال هناك،  فهذا جيد جدا. ولكن أولا يجب أن تحدد موعد مع بعض الأساتذة والقسم، ويجب أن تتناقش في الأبحاث أو يكون عندك مقترح بحثي حتى لا تضيع وقتهم.

خطاب القبول

بعد تقييم الجامعة والقسم لطلبك، يحدد القرار بالقبول أو الرفض. يوجد قبول مشروط لاستيفاء بعض المتطلبات مثل اللغة، تحديد مصدر الدخل، المنح، الخ. في حال استيفاء كافة المتطلبات، تصدر الجامعة خطاب قبول غير مشروط نهائي، وبهذا فقط يمكن التقديم على التأشيرة. يوجد شهادة تصدر من الجامعة تسمى CAS تستخدم في إجراءات التأشيرة، وتصدر فقط عند القبول الغير مشروط.

إجراءات التأشيرة (الفيزا)

بعد القبول، تصدر الجامعة شهادة الـ  CAS وهي شهادة قبول رسمية للاستخدام في التقديم على التأشيرة. بعض التخصصات تتطلب التقديم على شهادة أخرى [11] تسمى ATAS، وهي البرامج الدراسية التي بها علوم من الممكن استخدامها في تصنيع أسلحة. تلك الشهادة تستغرق من عدة أسابيع لأشهر.

بعد ذلك، يمكنك التقديم على التأشيرة. كافة المتطلبات توجد بموقع الحكومة لتأشيرة الطلاب [12]. تتضمن تكلفة التأشيرة مصاريف التقديم بالإضافة إلى التأمين الصحي الذي يشمل مدة الدراسة ككل. 

ما بعد التخرج

الحصول على شهادة من المملكة المتحدة يزيد فرص العمل (أو تكملة الدراسات العليا) خاصة إذا كانت الجامعة جيدة. توفر المملكة المتحدة تأشيرات خاصة للطلاب المتخرجين حديثا للعمل بها دون قيود كثيرة (مقارنة بالآخرين الذين لم يتخرجوا منها). فمثلا تأشيرة المتخرجين [13] تتراوح من سنتين إلى ثلاثة، ويسمح خلالها بالعمل (أو البحث عنه) بدون نظام الكفالة (أي أن تحصل على عقد عمل من شركة تدعم تأشيرتك).

المساعدة

سأكون سعيدا بمساعدة المتقدمين على التقديم على الجامعات والرد على الأسئلة حسب توفر الوقت. ولكن سأقدر أولا قبل سؤالي قراءة هذا المقال ودراسة مع به من مصادر ودراسة موقع الجامعة والقسم ومحركات البحث.

المصادر

[1] https://www.timeshighereducation.com/world-university-rankings/2023/world-ranking

[2] https://www.topuniversities.com/university-rankings/world-university-rankings/2023

[3] https://www.undergraduate.study.cam.ac.uk/apply/statistics

[4] https://globalscholarships.com/university-of-york-acceptance-rate/

[5] https://www.postgraduate.study.cam.ac.uk/courses/directory/cscspdpcs/requirements

[6] https://www.cs.york.ac.uk/postgraduate/research-degrees/phd/

[7] https://www.gov.uk/student-visa/money

[8] https://www.numbeo.com/cost-of-living

[9] https://www.britishcouncil.org.eg/en/programmes/education/science/british-council-scholarships-women-stem

[10] https://www.findaphd.com/phds/united-kingdom/computer-science/non-eu-students/

[11] https://www.gov.uk/guidance/academic-technology-approval-scheme

[12] https://www.gov.uk/student-visa

[13] https://www.gov.uk/graduate-visa

[14] https://www.britishcouncil.org.eg/en/programmes/education/newton-mosharafa-fund

[15] https://qalaascholarships.org/

[16] https://saidfoundation.org/apply/

[17] https://www.chevening.org/scholarships/

[18] https://www.isdb.org/scholarships

New sel4test and sel4bench releases supporting SiFive's Unleashed Platform

In Brief: New features:

• A new option to run seL4 in machine mode.
• Ported seL4 to QEMU's SiFiveU and virt platforms.
• DTB parsing in seL4 to read and use UARTs when available.
• Ported seL4 to run on VC707 FPGA Freedom Unleashed platform.
• Initial Benchmarking support in seL4.
• Initial sel4bench port that can measure IPC and trap timing.

Details:

seL4 in Machine mode

• Enables future virtualization efforts (e.g. running Linux in S-Mode)
• User level is not affected by this change
• Kernel works in physical memory (doesn't use MMU or TLBs)
• No "global" kernel mappings in this mode
• User can use the entire virtual address space
• This allows the seL4 to use and/or export devices (like UART) without the need to trap to riscv-pk

seL4 on SiFive/Freedom Unleashed

This platform is the same as spike with minor modifications to the memory layout in order to use 1 GiB DRAM mapped into 2-level page tables (instead of 1). It runs on:

• QEMU's sifiveu and virt platforms.
• Freedom Unleashed VC707 Dev Kit.
• Boom (modified to work with Freedom SDK).

DTB Parsing of UARTs

That was quite easy to do, by just copying riscv-pk code to the initial seL4's DTB code. It follow riscv-pk behaviour of trying to find UART devices before using HTIF. It currently supports riscv-pk's UART drivers (copied):

• SiFive's UART
• UART16550

In machine mode, it works just fine because there's no address translation. In supervisor mode, I had to map the whole UART (1GiB-padded) address in a 1 GiB page. This is just for simplicity, future improvements would be mapping it in a 4 KiB page and/or to use HTIF for kernel and UART for user-level.

Benchmarking support in seL4

Need to add timestamp function in the kernel to read cycles. Furthermore, I added Benchmarking system calls in libsel4 to allow user levels calls. This enables both generic and utilisation benchmarking in seL4.

sel4bench port

A very basic initial port to be able to measure IPC and Hardware traps. Results for this work are shown in my previous blog post.

Links

$repo init -u https://github.com/heshamelmatary/sel4riscv-manifest.git -m sel4test-18072018.xml


$repo init -u https://github.com/heshamelmatary/sel4riscv-manifest.git -m sel4bench-18072018.xml

IPC Performance of seL4 microkernel on RISC-V Platforms

I managed to get Freedom Unleashed U500 and Boom synthesized on VC707 FPGA Board. This motivated me to port seL4 to run there and do some microbenchmarking using sel4bench project.

Note that the seL4/RISC-V port is still a prototype, yet it can compete with ARM and x86.  The results are based on the following tools/revisions:

1. seL4 9.0.1 Release
2. sel4bench Perfomance Webpage (01/06/2018)
3. SiFive's Freedom Unleashed U500 VC707DevKit (d3c9a39)
4. SiFive's Freedom Unleashed Software Development Kit (547868)
5. Boom (Berkeley Out-of-Order RISC-V Processor): with minor modifications to run on FPGA (19e9e9a) 
6. riscv-tools --with-arch=rv64ima (8ad8d48) 
7. Vivado 2016.4 

IPC Performance on sel4bench (01/06/2018)

	Sabre I.mx6 (Cortex A9 @1GHz)	IA32 SkyLake @3.4GHz	X64 SkyLake @3.4GHz	Jetson TK1 (Cortex A15 @700MHz)	RISC-V Freedom Unleashed U500	RISC-V Boom (Default)
IPC microbenchmark, client->server	917.5	733	1480	955.5	517.9	549.7
IPC microbenchmark, server->client	306	216	776	554	551	553

Results are in cycles.

RISC-V RTEMS port is Upstream

Introduction

Having the RISC-V's GCC and Binutils upstream, as well as the increasing popularity and support RISC-V is getting pushed us to upstream RTEMS/RISC-V port, and it is gonna be part of the upcoming major RTEMS release.

RTEMS (The Real-Time Executive for Multiprocessor Systems) is a contemporary Real-time embedded OS, started as a project back in 1988. Since then, it has been used in space (e.g. by NASA), military, robotics and many other embedded applications.

This blog post gives a brief status of the porting efforts (that's upstream), as well as a quick how to build/run the port on Spike.

Status

[RTEMS Kernel/OS]

• Compatible with RISC-V priv-1.10.
• Has interrupt support.
• Only tested on Spike.
• Only timer ISR is handled.
• Uses HTIF for console IO, and power off.
• Works entirely in Machine mode, standalone (doesn't rely on bbl).
• Tier-2 RTEMS Architecture (For info about different RTEMS Tiers see this).
• BSD-2 License.
• Some of the code is copied from riscv-pk. 

The port is divided into 2 main parts:

• CPU Port (riscv32, and riscv64)
• General CPU port that can be used by different RISC-V-based boards. 
• Fairly complete (but not optimized) for single core systems.
• BSP port (Board Support Package).
• generic_riscv that runs on Spike.
• Only timer and console drivers are implemented.
• generic64_riscv 64-bit of generic_riscv.

Limitations

• No cache or MMU management.
• No FPU support.

 [RTEMS Source Builder] Toolchain

RTEMS has, maintains and tests its own toolchain for each CPU architecture (target), which relies on source code upstream from GNU (and others). For example, by using RSB to build RTEMS/RISC-V toolchain, RSB will fetch GCC and Binutils from GNU repos/servers, extract, build and install them for RTEMS. This is an example output after installing the RISC-V/RTEMS toolchain:

Installed riscv*-rtems toolchain (RSB)

We currently use the following revisions/releases for the RISC-V/RTEMS toolchain:

Tools built by RSB for riscv32

Furthermore, Spike/fesvr can be built using RSB (fetched from GitHub).

 [RTEMS Tester]

Scripts have been added to RTEMS Tester in order to be able to run the > 500 RTEMS tests on Spike. Currently, most of the tests pass on Spike.

Final output after running RTEMS Tester on riscv32 port

Stats

Binary sizes

With -Os flag:

minimum.exe (simplest RTEMS app that does nothing)

➜  build riscv32-rtems4.12-size riscv32-rtems4.12/c/riscv_generic/testsuites/samples/minimum/minimum.exe
   text    data     bss     dec     hex filename
  33944    8433 268393028       268435405       fffffcd riscv32-rtems4.12/c/riscv_generic/testsuites/samples/minimum/minimum.exe

hello.exe (Hello World App - Uses console driver, printf)

➜  build riscv32-rtems4.12-size riscv32-rtems4.12/c/riscv_generic/testsuites/samples/hello/hello.exe   
   text    data     bss     dec     hex filename
  75612    7768 268352004       268435384       fffffb8 riscv32-rtems4.12/c/riscv_generic/testsuites/samples/hello/hello.exe

ticker.exe (Uses clock driver and console driver, printf)

➜  build riscv32-rtems4.12-size riscv32-rtems4.12/c/riscv_generic/testsuites/samples/ticker/ticker.exe 
   text    data     bss     dec     hex filename
  66480    8744 268360196       268435420       fffffdc riscv32-rtems4.12/c/riscv_generic/testsuites/samples/ticker/ticker.exe

Tests 

RV32

Final output after running RTEMS Tester on riscv32 port

RV64

Final output after running RTEMS Tester on riscv64 port

Takeaways/TODOs

Hardware Platforms: We need to test on actual hardware in order to level up RISC-V/RTEMS port to a Tier-1 architecture (the highest, on par with ARM and x86). Issues with current RISC-V HW platforms (that I know):

• HiFive1: We had a student working on HiFive1 port this summer part of Google Summer of Code. The main challenge was the memory size limitation.
• FPGAs: Currently, I'm aware of the Rocket Chip as an FPGA/HW target. It relies on bbl as a bootloader. Furthermore, it changes to S-Mode before jumping to the payload entry. That's not the case for RTEMS as it works in M-Mode.
• Do you have a RISC-V HW implementation: Please get it touch, we need more RISC-V/HW BSPs (with reasonably big enough memory for RTEMS e.g. > 128KiB). Only M-Mode is needed (for CPU) and console/timer (for BSPs). It would be also great if it can be remotely powered off/reset (for RTEMS Tester).

SMP support: Adding SMP support is easy for OSes working in S-Mode (just calling sbi_xxx functions). However, I've not investigated yet how feasible it is to implement SMP support for M-Mode-based implementations.

QEMU: Hasn't been updated for a while (and not upstream), and the latest privileged mode is 1.9. Tried to run the port on it though, but didn't work.

GDB: Would be great if it's gonna be upstream soon (with target sim?). RSB tries to build GDB for all targets/architectures, which is used part of RTEMS Tester as well (and to run basic sample apps).

Bugs: Will try to go over failed tests from RTEMS Tester and try to fix the bugs, unless someone beats me to it.

Quick HowTo

 To build the tools from source, RTEMS Source Builder is needed.

$ git clone git://git.rtems.org/rtems-source-builder.git
$ cd rtems-source-builder

Setup development directories and export PATH:

$ mkdir -p ~/development/rtems
$ export PATH=$HOME/development/rtems/4.12/bin:$PATH
$ export RTEMS_DEV=$HOME/development/

[Build Toolchain]

RV32

rtems-source-builder git:(master) ✗ cd rtems/
$ ../source-builder/sb-set-builder --log=l-riscv32.txt --prefix=$RTEMS_DEV/rtems/4.12 4.12/rtems-riscv32

RV64

$ ../source-builder/sb-set-builder --log=l-riscv64.txt --prefix=$RTEMS_DEV/rtems/4.12 4.12/rtems-riscv64

[Build Spike]

rtems-source-builder git:(master) ✗ cd  bare
$ ../source-builder/sb-set-builder --log=spike --prefix=$RTEMS_DEV/rtems/4.12 devel/spike

[Build RTEMS]

Clone RTEMS:

 $ git clone git://git.rtems.org/rtems.git
 $ cd rtems && ./bootstrap -p && ./bootstrap 

To build generic_riscv BSP (32-bit)

$ cd .. && mkdir build && cd build
$ ../rtems/configure --target=riscv32-rtems4.12  --enable-rtemsbsp=riscv_generic --enable-tests=samples


To build generic64_riscv BSP (64-bit)

$ cd .. && mkdir build64 && cd build64
$ ../rtems/configure --target=riscv64-rtems4.12  --enable-rtemsbsp=riscv64_generic --enable-tests=samples

[Run RTEMS]

RV32


➜  build spike --isa=RV32IMAFDC -m0x10000000:0x10000000 riscv32-rtems4.12/c/riscv_generic/testsuites/samples/hello/hello.exe



RV64


hello.exe (Hello World App - Uses console driver, printf)




➜ build64 spike -m0x10000000:0x10000000 riscv64-rtems4.12/c/riscv64_generic/testsuites/samples/hello/hello.exe
*** BEGIN OF TEST HELLO WORLD ***
Hello World
*** END OF TEST HELLO WORLD ***

ticker.exe 

(Uses clock driver and console driver in a multithreading test)

➜ build64 spike -m0x10000000:0x10000000 riscv64 rtems4.12/c/riscv64_generic/testsuites/samples/ticker/ticker.exe
*** BEGIN OF TEST CLOCK TICK ***
TA1 - rtems_clock_get_tod - 09:00:00 12/31/1988
TA2 - rtems_clock_get_tod - 09:00:00 12/31/1988
TA3 - rtems_clock_get_tod - 09:00:00 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:05 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:10 12/31/1988
TA2 - rtems_clock_get_tod - 09:00:10 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:15 12/31/1988
TA3 - rtems_clock_get_tod - 09:00:15 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:20 12/31/1988
TA2 - rtems_clock_get_tod - 09:00:20 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:25 12/31/1988
TA3 - rtems_clock_get_tod - 09:00:30 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:30 12/31/1988
TA2 - rtems_clock_get_tod - 09:00:30 12/31/1988
*** END OF TEST CLOCK TICK ***

[Run RTEMS Tester]

 

RV32

➜  build $RTEMS_DEV/rtems/rtems-tools/tester/rtems-test --log=riscv_generic.txt --rtems-bsp=riscv_generic --rtems-tools=$RTEMS_DEV/rtems/4.12 --timeout=40 riscv32-rtems4.12/c/riscv_generic/testsuites

RV64

➜  build $RTEMS_DEV/rtems/rtems-tools/tester/rtems-test --log=riscv64_generic.txt --rtems-bsp=riscv64_generic --rtems-tools=$RTEMS_DEV/rtems/4.12 --timeout=40 riscv64-rtems4.12/c/riscv64_generic/testsuites

[Update] seL4/RISC-V SMP support | seL4/RISC-V Tutorials Release

Updates (since 03062017)

 

A new unofficial 24062017 release of seL4, libraries and seL4 Tutorials.

• SMP support, tested on Spike with 2 - 9 cores:
• seL4 is using a big kernel lock.
• Only reschedule IPI (set affinity) is provided.
• Relying on SBI to do other remote operations.
• SBI doesn't provide VADDR-> ASID -> HART operation.
• Using tp register to hold per-core IPC buffer addresses.
• Ported seL4-tutorias to RISC-V. This means:
• People can learn more about both seL4/RISC-V doing the tutorials.
• Lack of RISC-V/Spike user-level timer (or another S-timer) is an issue. seL4 (being a microkernel) is not supposed to provide a timer API, rather, user-level apps should have their own HW timer and device drivers.
• More tests are passing on sel4test now after:
• SMP support.
• Re-adding a supervisor timer (for seL4 scheduling).
• [154/154] Tests pass (8 more tests pass after multicore and timer support).
• All libraries, kernel are rebased to latest seL4's revisions.

seL4 Tutorials 

 

sel4-tutorials [1] is the first recommended entry point for people who want to learn and get hands-on experience on seL4 and its libraries.  This repo [1] contains slides, docs and code tutorials with commented instructions and tasks that take you from writing a seL4 hello world application to doing IPC in a multithreading environment, now on RISC-V.

hello-3 exercise showing 2 threads doing IPC communication

 [1] https://github.com/heshamelmatary/sel4-tutorials/tree/RISCVUnofficialRelease-24062017

seL4test

 

seL4test is a comprehensive unit and functional testing suite for seL4 and can be useful when porting to new platforms or adding new features.

It can be used as a reference how to develop a big project on seL4. A new riscv_smp_defconfig config file for RISC-V is added to test SMP support. Instructions how to run it are provided in this blog post.

For this release that contains SMP, use:

$repo init -u git@github.com:heshamelmatary/sel4riscv-manifest.git -m sel4test-24062017.xml

Note

 

This work is my personal/independent effort (during spare time) and it's not related to Data61/CSIRO/TS Group (that maintains seL4), until it gets upstream.

sel4test/RISC-V unofficial release - priv-1.10 - spec-2.3

Major updates since 2015

• - It's now based on seL4's master (rather than experimental) branch, which means it makes use of architecture-independent verified code.
• - Instead of earlier 32-bit support, it's now based on 64-bit RISC-V.
• - Compatible with latest RISC-V priv-1.10 and user-2.2/3 specs.
• - sel4test and libraries are ported and passing 146/146 tests.
• - Tested on Spike and Rocket Chip on FPGA soft-float (also previous version worked with QEMU 1.9.1).
• - Implements seL4's fastpath support.
• - 3 page mappings are supported (Sv39: 4KiB, 2MiB and 1GiB).
• - Relies on SBI from unmodified riscv-pk/bbl to emulate M-mode (same as riscv-linux).

Work in progress

• - Upstreaming seL4/RISC-V port.
• - Multicore support.
• - Research-wise, I've been working on adding CHERI support to RISC-V (Spike) as an extension, and aiming to experiment seL4 on it.

TODO list

• - Upstream the kernel (and libraries).
• - Add debug and benchmark support.
• - Release sel4bench.
• - Port sel4-tutorial to RISC-V (Start Guide for new comers/learners).
• - External interrupt handling and work with PLIC.

Quick How to

1. Install riscv64 tools (priv-1.10)
2. Get sel4test/RISC-V (using repo, for more info see [1])
3. $repo init -u git@github.com:heshamelmatary/sel4riscv-manifest.git -m sel4test-03062017.xml
   $repo sync 
4. $make riscv_defconfig && $make 
5. build riscv-pk/bbl with path to images/sel4test-driver-image-riscv-spike (from 4)
6.  run spike with bbl image generated from 5.

sel4test/RISC-V running on Spike

Note

This work is of my personal/independent effort (during spare-time) and it's not related to Data61/CSIRO/TS Group (that maintains seL4), until it gets upstreamed.

References

[1]  https://wiki.sel4.systems/Getting started